proposition: Lemma emb_fcycle_cycle p : fcycle face p -> cycle (--) [seq f z | z <- p].
proof: Proof. case: p => //= x p; rewrite -map_rcons; apply: homo_path => {x} x y /eqP<-. by rewrite -emb_edge // adjn_face. 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)