proposition: Lemma genM_join G H : <<G * H>> = G <*> H.
proof: Proof. apply/eqP; rewrite eqEsubset gen_subG /= -{1}[G <*> H]mulGid. rewrite genS; last by rewrite subUset mulG_subl mulG_subr. by rewrite mulgSS ?(sub_gen, subsetUl, subsetUr). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)