proposition: Lemma Mbeta_Hall : \beta(M).-Hall(M) M`_\beta.
proof: Proof. have [H hallH] := Hall_exists \beta(M) solM; have [sHM bH _]:= and3P hallH. rewrite [M`_\beta](sub_pHall hallH) ?pcore_pgroup ?pcore_sub //=. rewrite -(setIidPl sMbMs) pcore_setI_normal ?pcore_normal //. have sH: \sigma(M).-group H := sub_pgroup (beta_sub_sigma maxM) bH. have sHMs: H \subset M`_\sigma by rewrite (sub_Hall_pcore hallMs). rewrite -pcoreNK -bigcap_p'core subsetI sHMs. apply/bigcapsP=> p b'p; have [_ hallKp' _] := beta_max_pdiv b'p. by rewrite (sub_Hall_pcore hallKp') ?(pi_p'group bH). 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)