proposition: Lemma equiv_of_sub (T : finType) (e1 e2 : rel T) : subrel e1 e2 -> reflexive e2 -> symmetric e2 -> transitive e2 -> subrel (equiv_of e1) e2.
proof: Proof. move => sub2 refl2 sym2 trans2 x y. case/connectP => p. elim: p x => [x _ -> //|a p IHp x] /= /andP [/orP H] pth lst. apply: trans2 _ (IHp _ pth lst). case: H; last rewrite sym2; exact: sub2. Qed.
imports: Coq(RelationClasses Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries bij finite_quotient)