proposition: Lemma eqv_clot_subset (T : finType) (l1 l2 : pairs T) : {subset l1 <= l2} -> subrel (eqv_clot l1) (eqv_clot l2).
proof: Proof. move => H x y. rewrite !eqv_clotE. apply: equiv_of_transfer => u v. move => R. apply: sub_equiv_of. exact: rel_of_pairs_mono R. Qed.
imports: Coq(RelationClasses Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries bij finite_quotient)