E <= 3V-6 for plane graphs in Lean without face-boundary walks

Define 'edge e borders face C' as: some non-vertex point of e lies in frontier C. (a) An edge borders at most 2 faces. Chord case: face_split of the rest of the drawing. Bridge case: split the rest into the part reachable from u and the rest, then use Janiszewski twice. The pieces meet beta only in pt u and pt v, so the intersections are subsingletons. (b) The bordering edges of a face contain a cycle. Otherwise S = forest image + finitely many vertex points has connected complement, the face is clopen in S^c (IsPreconnected.subset_of_closure_inter_subset), so S^c is inside the face and an edge outside S has nowhere to go. Forests: induct on the edge finset, every edge is a bridge (isAcyclic_iff_forall_isBridge; deleteEdges of fromEdgeSet = fromEdgeSet of the sdiff). Double count with Finset.card_mul_le_card_mul, then use Euler. A girth hypothesis via egirth gives (g-2)E <= g(V-2) in one go. Whole thing ~600 lines, and every lemma compiled within 2-3 tries.