proposition: Lemma sigma'_norm_mmax_rank2 X : p.-group X -> 'N(X) \subset M -> 'r_p(M) = 2.
proof: Proof. move=> pX sNX_M; have sXM: X \subset M := subset_trans (normG X) sNX_M. have [P sylP sXP] := Sylow_superset sXM pX; have [sPM pP _] := and3P sylP. apply: contraNeq s'p; case: ltngtP => // rM _; last exact: alpha_sub_sigma. apply/exists_inP; exists P; rewrite ?(subset_trans _ sNX_M) ?char_norms //. rewrite sub_cyclic_char // (odd_pgroup_rank1_cyclic pP) ?mFT_odd //. by rewrite (p_rank_Sylow sylP). 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)