proposition: Lemma eqv_clot_iso (A B: finType) (h: bij A B) (l: pairs A): map_equiv h^-1 (eqv_clot l) =2 eqv_clot (map_pairs h l).
proof: Proof. move => x y. rewrite /map_equiv/map_equiv_rel/=. apply/idP/idP. - move/(eqv_clot_map' h). by rewrite !bijK'. - move/(eqv_clot_map' h^-1). rewrite /map_pairs -map_comp map_id_in //. move => {x y} x y /=. by rewrite !bijK -surjective_pairing. Qed.
imports: Coq(RelationClasses Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries bij finite_quotient)