proposition: Lemma homo_fpath_in {T T' : eqType} (h : T -> T') (f : T -> T) (f' : T' -> T') x s : {in belast x s, forall x : T, h (f x) = f' (h x)} -> fpath f x s -> fpath f' (h x) [seq h i | i <- s].
proof: Proof. elim: s x => //= u s IH x /all_cons [Hx {}/IH IH] /andP [/eqP fx path_s]. by rewrite -Hx fx IH ?eqxx. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)