proposition: Lemma group_modr A B G : B \subset G -> (G :&: A) * B = G :&: A * B.
proof: Proof. move=> sBG; apply: invg_inj; rewrite !(invMg, invIg) invGid !(setIC G). by rewrite group_modl // -invGid invSg. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)