proposition: Lemma sigma'_rank2_max : 'r_p(M) = 2 -> 'E_p^2(M) \subset 'E*_p(G).
proof: Proof. move=> rpM; apply: contraR s'p => /subsetPn[A Ep2A not_maxA]. have{Ep2A} [sAM abelA dimA] := pnElemP Ep2A; have [pA _ _] := and3P abelA. have [P sylP sAP] := Sylow_superset sAM pA; have [_ pP _] := and3P sylP. apply/exists_inP; exists P; rewrite ?uniq_mmax_norm_sub //. apply: def_uniq_mmaxS (mFT_pgroup_proper pP) (def_uniq_mmax _ _ sAM) => //. by rewrite (@nonmaxElem2_Uniqueness _ p) // !(not_maxA, inE) abelA dimA subsetT. 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)