proposition: Lemma Ohm1_ucn_p2maxElem E : E \in 'E_p^2(R) :&: 'E*_p(R) -> [/\ ~~ (E \subset T), #|Z| = p /\ [group of W] \in 'E_p^2(R) & T \char R /\ #|R : T| = p ].
proof: Proof. case/setIP=> Ep2E maxE; have defCRE1 := Ohm1_cent_max maxE pR. have [[sER abelE dimE] oE] := (pnElemP Ep2E, card_pnElem Ep2E). have [[sZR_R nZR_R] [pE _ eE]] := (andP (center_normal R), and3P abelE). have{nZR_R} nZR: R \subset 'N(Z) := gFnorm_trans _ nZR_R. have{sZR_R} [pZR pW] := (pgroupS sZR_R pR, pgroupS sWR pR). have sZE: Z \subset E by rewrite -defCRE1 OhmS ?setIS // centS. have rCRE : 'r_p('C_R(E)) = 2 by rewrite -p_rank_Ohm1 defCRE1 p_rank_abelem. have oZ: #|Z| = p. apply/prime_nt_dvdP; rewrite -?trivg_card1 // (card_pgroup pZ) /= -/Z. rewrite (@dvdn_exp2l _ _ 1) // -ltnS -dimE properG_ltn_log //= -/Z. by case/eqVproper: sZE rR => // defZ; rewrite -defCRZ defZ rCRE ltnn. have ncycR: ~~ cyclic R by rewrite (odd_pgroup_rank1_cyclic pR) // -(subnKC rR). have [ncycW eW] := Ohm1_odd_ucn2 pR oddR ncycR; rewrite -/W in ncycW eW. have sWRZ: [~: W, R] \subset Z. rewrite [Z](OhmE 1 pZR) sub_gen //= -ucn1 subsetI. rewrite (subset_trans _ (ucn_comm 1 _)) ?commSg ?Ohm_sub //. by move: nWR eW; rewrite -commg_subl -sub_LdivT; apply: subset_trans. have sZW: Z \subset W by rewrite OhmS /= -?ucn1 ?ucn_subS //. have ltZW: Z \proper W. by rewrite properEneq; case: eqP ncycW => // <-; rewrite prime_cyclic ?oZ. have sWRE := subset_trans sWRZ sZE. have nEW: W \subset 'N(E) by rewrite -commg_subr (subset_trans _ sWRE) ?commgSS. have defZ: 'C_W(E) = Z. have sCE: 'C_W(E) \subset E. rewrite -{2}defCRE1 (OhmE 1 (pgroupS (subsetIl R _) pR)) sub_gen //. by rewrite subsetI setSI // subIset // sub_LdivT eW. have [defC | ltCE] := eqVproper sCE. have sEW: E \subset W by rewrite -defC subsetIl. have nsER: E <| R. by rewrite /normal sER -commg_subl (subset_trans (commSg R sEW)). have [B scn3B sEB] := normal_p2Elem_SCN3 Ep2E nsER. have [scnB dimB] := setIdP scn3B; have [_ scBR] := SCN_P scnB. rewrite ltnNge -rank_Ohm1 -dimE -rank_abelem ?rankS // in dimB. by rewrite -scBR -defCRE1 OhmS // setIS ?centS. apply/eqP; rewrite eq_sym eqEcard oZ (card_pgroup (pgroupS sCE pE)) /= -/W. rewrite subsetI sZW (centsS sER); last by rewrite centsC -subsetIidl defCRZ. by rewrite (leq_exp2l _ 1) // -ltnS -dimE properG_ltn_log. have dimW: logn p #|W| = 2. apply/eqP; rewrite -(Lagrange sZW) lognM ?cardG_gt0 // oZ (pfactorK 1) //=. rewrite -/Z eqSS eqn_leq -{1}defZ logn_quotient_cent_abelem ?dimE // -/W. by rewrite -divgS // logn_div ?cardSg // subn_gt0 properG_ltn_log. have abelW: p.-abelem W. by rewrite (abelem_Ohm1 (pgroupS _ pR)) ?(p2group_abelian pW) ?dimW ?ucn_sub. have charT: T \char R by rewrite subcent_char ?char_refl ?gFchar_trans. rewrite 2!inE sWR abelW dimW; do 2?split => //. by apply: contra (proper_subn ltZW); rewrite -defZ !subsetI subxx sER centsC. apply/prime_nt_dvdP=> //. rewrite indexg_eq1 subsetIidl centsC; apply: contraFN (ltnn 1) => cRW. by rewrite -dimW -(setIidPl (centsS sER cRW)) defZ oZ (pfactorK 1). rewrite -(part_pnat_id (pnat_dvd (dvdn_indexg _ _) pR)) p_part. by rewrite (@dvdn_exp2l p _ 1) ?logn_quotient_cent_abelem ?dimW. 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)