proposition: Lemma Mbeta_quo_nil : nilpotent (M^`(1) / M`_\beta).
proof: Proof. have /and3P[_ bMb b'M'Mb] := pHall_subl Mbeta_der1 sM'M Mbeta_Hall. apply: nilpotentS (Fitting_nil (M^`(1) / M`_\beta)) => /=. rewrite -{1}[_ / _]Sylow_gen gen_subG. apply/bigcupsP=> Q /SylowP[q _ /and3P[sQM' qQ _]]. apply: subset_trans (pcore_sub q _). rewrite p_core_Fitting -pcoreNK -bigcap_p'core subsetI sQM' /=. apply/bigcapsP=> [[p /= _] q'p]; have [b_p | b'p] := boolP (p \in \beta(M)). by rewrite pcore_pgroup_id ?(pi'_p'group _ b_p) // /pgroup card_quotient. have p'Mb: p^'.-group M`_\beta := pi_p'group bMb b'p. rewrite sub_Hall_pcore ?(pi_p'group qQ) {Q qQ sQM'}//. rewrite pquotient_pcore ?quotient_pHall 1?gFsub_trans //. by have [-> _ _] := beta_max_pdiv b'p. 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)