proposition: Lemma equiv_ofE (T1 T2 : finType) (e1 : rel T1) (e2 : equiv_rel T2) (f : T1 -> T2) x y : (forall u v : T1, e1 u v -> e2 (f u) (f v)) -> equiv_of e1 x y -> e2 (f x) (f y).
proof: Proof. move => H. case/connectP => p. elim: p x => /= [x _ -> //|z p IH x /andP [xz] pth_p lst_p]. apply: equiv_trans (IH _ pth_p lst_p). case/orP : xz; [exact: H|rewrite equiv_sym; exact: H]. Qed.
imports: Coq(RelationClasses Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries bij finite_quotient)