proposition: Lemma homo_cycle (aT rT : Type) (f : aT -> rT) (e1 : rel aT) (e2 : rel rT) (s : seq aT) : {homo f : x y / e1 x y >-> e2 x y} -> cycle e1 s -> cycle e2 (map f s).
proof: Proof. case: s => //= a s hom_f; rewrite !rcons_path => /andP [pth_s /hom_f lst_s]. by rewrite (homo_path hom_f pth_s) last_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)