proposition: Lemma group_modl A B G : A \subset G -> A * (B :&: G) = A * B :&: G.
proof: Proof. move=> sAG; apply/eqP; rewrite eqEsubset subsetI mulgS ?subsetIl //. rewrite -{2}mulGid mulgSS ?subsetIr //. apply/subsetP => _ /setIP[/mulsgP[a b Aa Bb ->] Gab]. by rewrite mem_mulg // inE Bb -(groupMl _ (subsetP sAG _ Aa)). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)