proposition: Proposition beta_norm_sub_mmax M Y : M \in 'M -> \beta(M).-subgroup(M) Y -> Y :!=: 1 -> 'N(Y) \subset M.
proof: Proof. move=> maxM /andP[sYM bY] ntY. have [F1 | [q q_pr q_dv_FY]] := trivgVpdiv 'F(Y). by rewrite -(trivg_Fitting (solvableS sYM (mmax_sol maxM))) F1 eqxx in ntY. pose X := 'O_q(Y); have qX: q.-group X := pcore_pgroup q _. have ntX: X != 1. apply: contraTneq q_dv_FY => X1; rewrite -p'natE // -partn_eq1 //. rewrite -(card_Hall (nilpotent_pcore_Hall q (Fitting_nil Y))). by rewrite /= p_core_Fitting -/X X1 cards1. have bMq: q \in \beta(M) by apply: (pgroupP (pgroupS (Fitting_sub Y) bY)). have b_q: q \in \beta(G) by move: bMq; rewrite -predI_sigma_beta //; case/andP. have sXM: X \subset M := gFsub_trans _ sYM. have [P sylP sXP] := Sylow_superset sXM qX; have [sPM qP _] := and3P sylP. have sylPG: q.-Sylow(G) P by rewrite (sigma_Sylow_G maxM) ?beta_sub_sigma. have uniqNX: 'M('N_P(X)) = [set M]. apply: def_uniq_mmax => //; last by rewrite subIset ?sPM. exact: (beta_subnorm_uniq b_q). rewrite (subset_trans (char_norms (pcore_char q Y))) //. rewrite (sub_uniq_mmax uniqNX) ?subsetIr // mFT_norm_proper //. by rewrite (sub_mmax_proper maxM). 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)