proposition: Lemma equiv_of_sub' (T : finType) (e1 : rel T) (e2 : equiv_rel T) : subrel e1 e2 -> subrel (equiv_of e1) e2.
proof: Proof. move => sub. apply: equiv_of_sub => //; auto using equiv_sym, equiv_trans. Qed.
imports: Coq(RelationClasses Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries bij finite_quotient)