proposition: Theorem exceptional_sigma_nil : nilpotent M`_\sigma.
proof: Proof. have [g nPg notMg] := subsetPn not_sNP_M. set Ms := M`_\sigma; set F := Ms <*> A0 :^ g. have sA0gM: A0 :^ g \subset M. by rewrite (subset_trans _ sPM) // -(normP nPg) conjSg (subset_trans sA0A). have defF: Ms ><| A0 :^ g = F. rewrite sdprodEY ?coprime_TIg //. by rewrite (subset_trans sA0gM) ?gFnorm. by rewrite cardJg oA0 (pnat_coprime (pcore_pgroup _ _)) ?pnatE. have regA0g: 'C_Ms(A0 :^ g) = 1. case/exceptional_TI_MsigmaJ: notMg => //. by rewrite -sub_conjgV (subset_trans _ sPM) // sub_conjgV (normP _). rewrite (prime_Frobenius_sol_kernel_nil defF) ?cardJg ?oA0 //. by rewrite (solvableS _ (mmax_sol maxM)) // join_subG pcore_sub. 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 BGsection10)