proposition: Lemma group_setX (H1 : {group gT1}) (H2 : {group gT2}) : group_set (setX H1 H2).
proof: Proof. apply/group_setP; split; first by rewrite !inE !group1. by case=> [x1 x2] [y1 y2] /[!inE] /andP[Hx1 Hx2] /andP[Hy1 Hy2] /[!groupM]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)