fact: Definition eqv_clot (T : finType) (l : pairs T) : equiv_rel T := locked [equiv_rel of equiv_of (rel_of_pairs l)].
imports: Coq(RelationClasses Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries bij finite_quotient)