proposition: Lemma connect_transfer x y : connect e x y = connect e' (f x) (f y).
proof: Proof. Proof using f_eq f_inj f_inv. apply/idP/idP. - case/connectP => s. elim: s x => //= [x _ -> |z s IH x]; first exact: connect0. case/andP => xz pth Hy. rewrite f_eq in xz. apply: connect_trans (connect1 xz) _. exact: IH. - case/connectP => s. elim: s x => //= [x _ /f_inj -> |z s IH x]; first exact: connect0. case/andP => xz pth Hy. case: (f_inv xz) => z' ?; subst. rewrite -f_eq in xz. apply: connect_trans (connect1 xz) _. exact: IH. Qed.
imports: mathcomp(all_ssreflect)