proposition: Lemma setX_gen (H1 : {set gT1}) (H2 : {set gT2}) : 1 \in H1 -> 1 \in H2 -> <<setX H1 H2>> = setX <<H1>> <<H2>>.
proof: Proof. move=> H1_1 H2_1; apply/eqP. rewrite eqEsubset gen_subG setXS ?subset_gen //. rewrite -[in X in X \subset _]setX_prod. rewrite -morphim_pair1g -morphim_pairg1 !morphim_gen ?subsetT //. by rewrite morphim_pair1g morphim_pairg1 mul_subG // genS // setXS ?sub1set. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)