proposition: Lemma pgroupM pi G H : pi.-group (G * H) = pi.-group G && pi.-group H.
proof: Proof. have GH_gt0: 0 < #|G :&: H| := cardG_gt0 _. rewrite /pgroup -(mulnK #|_| GH_gt0) -mul_cardG -(LagrangeI G H) -mulnA. by rewrite mulKn // -(LagrangeI H G) setIC !pnatM andbCA; case: (pnat _). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype bigop finset prime fingroup morphism) mathcomp(gfunctor automorphism quotient action gproduct) mathcomp(cyclic)