proposition: Lemma rel_of_pairs_mono (T : finType) (l l' : pairs T) : {subset l <= l'} -> subrel (rel_of_pairs l) (rel_of_pairs l').
proof: Proof. move => sub_l x y. exact: sub_l. Qed.
imports: Coq(RelationClasses Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries bij finite_quotient)