proposition: Lemma hiso_fconnect (f : G -> G) (f' : H -> H) : (forall x, i (f x) = f' (i x)) -> forall x y, fconnect f x y = fconnect f' (i x) (i y).
proof: Proof. move => com x y. apply: rel_functor. apply: (comm_adj H). 2: done. by move => {x y} x y; rewrite /= -com inj_eq. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)