proposition: Lemma equiv_of_ff x y : equiv_of e2 (f x) (f y) = equiv_of e1 x y.
proof: Proof. apply/idP/idP. - case/connectP => p. elim: p x => /= [|u' p IH] x. + by move => _ /f_inj ->. + case/andP => A B C. case/orP : A => A. * move/eq2E : (A) => [?] [v] [_ ?]. subst. apply: connect_trans (connect1 _) (IH _ B C). by rewrite /= !eq_e A. * move/eq2E : (A) => [v] [?] [? _]. subst. apply: connect_trans (connect1 _) (IH _ B C). by rewrite /= !eq_e A orbT. - apply: equiv_of_transfer => {x y} u v H. apply: sub_equiv_of. by rewrite -eq_e. Qed.
imports: Coq(RelationClasses Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries bij finite_quotient)