proposition: Lemma diso_face (G H : sgraph) (g : plane_embedding G) (i : diso G H) s : sface g s <-> sface (diso_plane_embedding g i) (map i s).
proof: Proof. apply: iff_exists => d /=. rewrite map_comp [map _ _ = _](rwP eqP) inj_eq -?(rwP eqP) //. exact: inj_map. 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)