proposition: Lemma exercise6_6a G H: equivalence G -> equivalence H -> (equivalence (G \cg H) <-> (G \cg H = H \cg G)).
proof: Proof. move=> eG eH. set (K:= G \cg H). split. move => eK. have aux a b: inc (J a b) K -> inc (J b a) K by move => h;equiv_tac. set_extens x => xK. have px: (pairp x) by apply: (@compg_graph G H). move: xK ; rewrite - px => /aux. move /compg_pP=> [y JH JG]; apply/compg_pP; exists y => //; equiv_tac. move: xK =>/compg_P [px [y JG JH]]. rewrite - px; apply: aux; apply/compg_pP;exists y => //; equiv_tac. move=> eq. move: eG eH; rewrite ! equivalence_pr. move=> [GG iG] [HH iH]; split. by rewrite {2} /K compgA eq - (compgA H G G) GG - compgA -/K eq compgA HH. by rewrite {2}/K compg_inverse -iH -iG. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)