proposition: Theorem tau2_Msigma_nil M p : M \in 'M -> p \in \tau2(M) -> nilpotent M`_\sigma.
proof: Proof. move=> maxM t2Mp; have [sM'p /eqP rpM] := andP t2Mp. have [A Ep2A] := p_rank_witness p M; rewrite rpM in Ep2A. have [_]:= p2Elem_mmax maxM Ep2A; rewrite -negb_exists_in [p \in _](negPf sM'p). have [[A0 EpA0 /eqP/mem_uniq_mmax[_ sNA0M _]] | _ [] //] := exists_inP. have{EpA0 sNA0M} excM: exceptional_FTmaximal p M A0 A by []. have [sAM abelA _] := pnElemP Ep2A; have [pA _] := andP abelA. have [P sylP sAP] := Sylow_superset sAM pA. exact: exceptional_sigma_nil maxM excM sylP sAP. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq choice div fintype) mathcomp(path bigop finset prime fingroup morphism perm automorphism) mathcomp(quotient action gproduct gfunctor pgroup cyclic commutator) mathcomp(center gseries nilpotent sylow abelian maximal hall frobenius) odd_order(BGsection1 BGsection3 BGsection4 BGsection5 BGsection6) odd_order(BGsection7 BGsection9 BGsection10 BGsection11)