proposition: Lemma mul_subG A B : A \subset G -> B \subset G -> A * B \subset G.
proof: Proof. by move=> sAG sBG; rewrite -mulGid mulgSS. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)