proposition: Lemma eqv_clot_cat (A: finType) (h k: pairs A): equiv_comp (eqv_clot (map_pairs (pi (eqv_clot h)) k)) =2 eqv_clot (h++k).
proof: Proof. move => x y. symmetry. rewrite /equiv_comp map_equivE/= !eqv_clotE /=. set e1 := rel_of_pairs _. set e2 := rel_of_pairs _. apply/idP/idP. - apply: equiv_of_transfer => {x y} u v. rewrite /e1/rel_of_pairs/= mem_cat. case/orP => H. + apply: eq_equiv. apply/eqquotP. rewrite eqv_clotE. exact: sub_equiv_of. + apply: sub_equiv_of. apply/mapP. by exists (u,v). - suff S (u v : quot (eqv_clot h)): equiv_of e2 u v -> equiv_of e1 (repr u) (repr v). { move/S => H. apply: equiv_trans (equiv_trans _ _). 2: exact: H. rewrite /= -eqv_clotE. exact: (eqv_clot_subset h) (piK' _ _). rewrite /= -eqv_clotE equiv_sym. exact: (eqv_clot_subset h) (piK' _ _). } apply: equiv_of_transfer => {u v} u v /mapP [[u0 v0] H0] [-> ->]. apply: equiv_trans (equiv_trans _ _). 2:{ rewrite /= -eqv_clotE. apply: (eqv_clot_subset k) _. done. rewrite eqv_clotE. apply: sub_equiv_of. exact: H0. } rewrite equiv_sym. all: rewrite /= -eqv_clotE; exact: (eqv_clot_subset h) (piK' _ _). Qed.
imports: Coq(RelationClasses Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries bij finite_quotient)