proposition: Lemma emb_face_cycle (x : D) : cycle (--) [seq f z | z <- orbit face x].
proof: Proof. exact/emb_fcycle_cycle/cycle_orbit/faceI. 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)