proposition: Lemma setX_prod (H1 : {set gT1}) (H2 : {set gT2}) : setX H1 1 * setX 1 H2 = setX H1 H2.
proof: Proof. apply/setP=> [[x y]]; rewrite !inE /=. apply/imset2P/andP=> [[[x1 u1] [v1 y1]] | [Hx Hy]]. rewrite !inE /= => /andP[Hx1 /eqP->] /andP[/eqP-> Hx] [-> ->]. by rewrite mulg1 mul1g. exists (x, 1 : gT2) (1 : gT1, y); rewrite ?inE ?Hx ?eqxx //. by rewrite /mulg /= /extprod_mulg /= mulg1 mul1g. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)