proposition: Lemma normal_p2Elem_SCN3 E : E \in 'E_p^2(R) -> E <| R -> exists2 B, B \in 'SCN_3(R) & E \subset B.
proof: Proof. move=> Ep2E /andP[sER nER]; have [_ abelE dimE] := pnElemP Ep2E. have [B Ep3B nBR]: exists2 B, B \in 'E_p^3(R) & R \subset 'N(B). have [C] := rank3_SCN3; case/setIdP=> SCN_C rC. have [nsCR cCC] := andP (maxgroupp (SCN_max SCN_C)). have [sCR _] := andP nsCR; have pC: p.-group C := pgroupS sCR pR. have{pC cCC} abelC1: p.-abelem 'Ohm_1(C) := Ohm1_abelem pC cCC. have dimC1: 3 <= logn p #|'Ohm_1(C)| by rewrite -rank_abelem // rank_Ohm1. have nsC1R: 'Ohm_1(C) <| R := gFnormal_trans _ nsCR. have [B [sBC1 nsBR oB]] := normal_pgroup pR nsC1R dimC1. have [sBR nBR] := andP nsBR; exists B => //; apply/pnElemP. by rewrite oB pfactorK // (abelemS sBC1). have [sBR abelB dimB] := pnElemP Ep3B; have [pB cBB _] := and3P abelB. have [oB oE] := (card_pnElem Ep3B, card_pnElem Ep2E). pose Bs := (E <*> 'C_B(E))%G; have sCB: 'C_B(E) \subset B := subsetIl B _. have sBsR: Bs \subset R by rewrite join_subG sER subIset ?sBR. suffices Bs_gt2: 2 < logn p #|Bs|. have nBsR: Bs <| R by rewrite /normal sBsR // normsY ?normsI ?norms_cent. have abelBs: p.-abelem Bs. by rewrite (cprod_abelem p (cprodEY _)) ?subsetIr // abelE (abelemS sCB). have [C maxC sBsC] : {H | [max H | H <| R & abelian H ] & Bs \subset H}. by apply: maxgroup_exists; rewrite nBsR (abelem_abelian abelBs). exists C; last by rewrite (subset_trans _ sBsC) ?joing_subl. by rewrite inE (max_SCN pR) ?(leq_trans Bs_gt2) // -rank_abelem ?rankS. apply: contraFT (ltnn 2); rewrite -leqNgt => Bs_le2. have{Bs_le2} sCE: 'C_B(E) \subset E. rewrite (sameP joing_idPl eqP) eq_sym eqEcard joing_subl /=. by rewrite (card_pgroup (pgroupS sBsR pR)) oE leq_exp2l. have dimCBE: 2 <= logn p #|'C_B(E)|. rewrite -ltnS -dimB -addn1 -leq_subLR -logn_div ?divgS ?cardSg //. by rewrite logn_quotient_cent_abelem ?dimE ?(subset_trans sBR nER). have defE: 'C_B(E) = E. apply/eqP; rewrite eqEcard sCE oE /=. by rewrite (card_pgroup (pgroupS sCB pB)) leq_exp2l. by rewrite -dimB -dimE -defE lognSg // subsetIidl sub_abelian_cent // -defE. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype finset prime fingroup morphism perm automorphism action) mathcomp(quotient cyclic gfunctor pgroup gproduct center commutator) mathcomp(gseries nilpotent sylow abelian maximal hall) odd_order(BGsection1 BGsection4)