proposition: Lemma ex_odd_normal_p2Elem : {S : {group gT} | S <| R & S \in 'E_p^2(R)}.
proof: Proof. have [M minM]: {M | [min M | M <| R & ~~ cyclic M]}. by apply: ex_mingroup; exists R; rewrite normal_refl. have{minM} [[nsMR ncycM] [_ minM]] := (andP (mingroupp minM), mingroupP minM). have [sMR _] := andP nsMR; have pM := pgroupS sMR pR. exists ('Ohm_1(M))%G; first exact: gFnormal_trans. apply: (subsetP (pnElemS _ _ sMR)). have [M1 | ntM] := eqsVneq M 1; first by rewrite M1 cyclic1 in ncycM. have{ntM} [p_pr _ [e oM]] := pgroup_pdiv pM ntM. have le_e_M: e <= logn p #|M| by rewrite ltnW // oM pfactorK. have{le_e_M} [N [sNM nsNR] oN] := normal_pgroup pR nsMR le_e_M. have ltNM: ~~ (#|N| >= #|M|) by rewrite -ltnNge oM oN ltn_exp2l ?prime_gt1. have cycN : cyclic N by apply: contraR ltNM => ncycN; rewrite minM //= nsNR. case/cyclicP: cycN => x defN; have Mx : x \in M by rewrite -cycle_subG -defN. apply: Ohm1_extremal_odd Mx _; rewrite ?(oddSg sMR) //. by rewrite -divgS /= -defN // oM oN expnS mulnK // expn_gt0 prime_gt0. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype finfun bigop ssralg finset prime binomial) mathcomp(fingroup morphism automorphism perm quotient action gproduct) mathcomp(gfunctor commutator zmodp cyclic center pgroup gseries nilpotent) mathcomp(sylow abelian maximal extremal hall) mathcomp(matrix mxalgebra mxrepresentation mxabelem) odd_order(BGsection1 BGsection2)