proposition: Lemma sface_cyle s : sface s -> cycle (--) s.
proof: Proof. case => d ->. apply: homo_cycle (cycle_orbit faceI _). move => x y /=. rewrite -emb_edge // => /eqP <-. exact: 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)