proposition: Lemma del_vertex_neighbor_face : exists2 s : seq G', sface g' s & {subset N(x) <= map val s}.
proof: Proof. have fdN : face d \notin N. { apply: wheel_proof => //. - apply: plane_emb_plain. - apply: plane_emb_loopless. } set d' : D' := Sub (face d) fdN; set s := [seq g' i | i <- orbit face d']. have H := @neighbor_face_aux D d _ _ simpleD nxxF. exists s; first by exists d'. move => z; rewrite inE /s -map_comp => xz. apply/mapP. rewrite -[x](pinvK g) -[z](pinvK g) -plane_emb_edge -[pinv g x]/d in xz. have cycleD : forall x y : D, x != y -> cface x y -> ~~ cnode x y. { apply: two_connected_cyle => //. apply: two_connected_avoid_one (emb_embedding g) connG. - exact: plane_emb_plain. - exact: plane_emb_loopless. - exact: emb_planar. } have := @del_node_adjn_face D d (plane_emb_plain g) (plane_emb_loopless g) simpleD nxxF cycleD. move=> /(_ _ xz) => -[dz]; rewrite [wheel_proof _ _ _ _ _ ](bool_irrelevance _ fdN). case => D1 D2. by exists dz => //=; apply/eqP; rewrite -[z](pinvK g) -plane_emb_vertex cnodeC. Qed.
imports: mathcomp(all_ssreflect) fourcolor(hypermap geometry color coloring walkup combinatorial4ct cfmap) GraphTheory(edone preliminaries bij digraph sgraph) GraphTheory(connectivity minor hmap_ops smerge hcycle arc)