proposition: Theorem Msigma_neq1 : M`_\sigma :!=: 1.
proof: Proof. without loss Ma1: / M`_\alpha = 1. by case: eqP => // Ms1 -> //; apply/trivgP; rewrite -Ms1 Malpha_sub_Msigma. have{Ma1} rFM: 'r('F(M)) <= 2. rewrite (leq_trans _ Malpha_quo_rank2) // Ma1. by rewrite -(isog_rank (quotient1_isog _)) rankS ?Fitting_sub. pose q := max_pdiv #|M|; pose Q := 'O_q(M)%G. have sylQ: q.-Sylow(M) Q := rank2_max_pcore_Sylow (mFT_odd M) solM rFM. have piMq: q \in \pi(M) by rewrite pi_max_pdiv cardG_gt1 mmax_neq1. have{piMq} ntQ: Q :!=: 1 by rewrite -rank_gt0 (rank_Sylow sylQ) p_rank_gt0. rewrite (subG1_contra _ ntQ) ?(sub_Hall_pcore Msigma_Hall) ?pcore_sub //. rewrite (pi_pgroup (pcore_pgroup _ _)) //; apply/exists_inP; exists Q => //. by rewrite (mmax_normal maxM) ?pcore_normal. 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)