proposition: Theorem Msigma_Hall_G : \sigma(M).-Hall(G) M`_\sigma.
proof: Proof. rewrite pHallE subsetT /= eqn_dvd {1}(card_Hall Msigma_Hall). rewrite partn_dvd ?cardG_gt0 ?cardSg ?subsetT //=. apply/dvdn_partP; rewrite ?part_gt0 // => p. rewrite pi_of_part ?cardG_gt0 // => /andP[_ s_p]. rewrite partn_part => [|q /eqnP-> //]. have [P sylP] := Sylow_exists p M; have [sPM pP _] := and3P sylP. rewrite -(card_Hall (sigma_Sylow_G _ _ sylP)) ?cardSg //. by rewrite (sub_Hall_pcore Msigma_Hall) ?(pi_pgroup pP). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div path fintype) mathcomp(bigop finset prime fingroup morphism perm automorphism quotient) mathcomp(action gproduct gfunctor pgroup cyclic center commutator) mathcomp(gseries nilpotent sylow abelian maximal hall) odd_order(BGsection1 BGsection3 BGsection4 BGsection5 BGsection6) odd_order(BGsection7 BGsection9)