proposition: Lemma face_preim (G : sgraph) (g : plane_embedding G) (x0 : emb_map g) (p := orbit face x0) x (s : seq G) : s = [seq g x | x <- p] -> x \in s -> exists2 d, d \in p & x = g d.
proof: Proof. by move=> -> /mapP. 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)