proposition: Lemma setX_dprod (H1 : {group gT1}) (H2 : {group gT2}) : setX H1 1 \x setX 1 H2 = setX H1 H2.
proof: Proof. rewrite dprodE ?setX_prod //. apply/centsP=> [[x u]] /[!inE]/= /andP[/eqP-> _] [v y]. by rewrite !inE /= => /andP[_ /eqP->]; congr (_, _); rewrite ?mul1g ?mulg1. apply/trivgP; apply/subsetP=> [[x y]]; rewrite !inE /= -!andbA. by case/and4P=> _ /eqP-> /eqP->; rewrite eqxx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)