proposition: Lemma homo_connect (aT rT : finType) (e : rel aT) (e' : rel rT) (f : aT -> rT) a b : {homo f : x y / e x y >-> e' x y} -> connect e a b -> connect e' (f a) (f b).
proof: Proof. move => hom_f; case/connectP => p p1 p2; apply/connectP. exists (map f p); by [exact: homo_path p1|rewrite last_map -p2]. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)