proposition: Lemma pmaxElem_extraspecial : 'E*_p(G) = 'E_p^('r_p(G))(G).
proof: Proof. have sZmax: {in 'E*_p(G), forall E, 'Z(G) \subset E}. move=> E maxE; have defE := pmaxElem_LdivP p_pr maxE. have abelZ: p.-abelem 'Z(G) by rewrite prime_abelem ?oZ. rewrite -(Ohm1_id abelZ) (OhmE 1 (abelem_pgroup abelZ)) gen_subG -defE. by rewrite setSI // setIS ?centS // -defE !subIset ?subxx. suffices card_max: {in 'E*_p(G) &, forall E F, #|E| <= #|F| }. have EprGmax: 'E_p^('r_p(G))(G) \subset 'E*_p(G) := p_rankElem_max p G. have [E EprE]:= p_rank_witness p G; have maxE := subsetP EprGmax E EprE. apply/eqP; rewrite eqEsubset EprGmax andbT; apply/subsetP=> F maxF. rewrite inE; have [-> _]:= pmaxElemP maxF; have [_ _ <-]:= pnElemP EprE. by apply/eqP; congr (logn p _); apply/eqP; rewrite eqn_leq !card_max. move=> E F maxE maxF; set U := E :&: F. have [sUE sUF]: U \subset E /\ U \subset F by apply/andP; rewrite -subsetI. have sZU: 'Z(G) \subset U by rewrite subsetI !sZmax. have [EpE _]:= pmaxElemP maxE; have{EpE} [sEG abelE] := pElemP EpE. have [EpF _]:= pmaxElemP maxF; have{EpF} [sFG abelF] := pElemP EpF. have [V] := abelem_split_dprod abelE sUE; case/dprodP=> _ defE cUV tiUV. have [W] := abelem_split_dprod abelF sUF; case/dprodP=> _ defF _ tiUW. have [sVE sWF]: V \subset E /\ W \subset F by rewrite -defE -defF !mulG_subr. have [sVG sWG] := (subset_trans sVE sEG, subset_trans sWF sFG). rewrite -defE -defF !TI_cardMg // leq_pmul2l ?cardG_gt0 //. rewrite -(leq_pmul2r (cardG_gt0 'C_G(W))) mul_cardG. rewrite card_subcent_extraspecial // mulnCA Lagrange // mulnC. rewrite leq_mul ?subset_leq_card //; last by rewrite mul_subG ?subsetIl. apply: subset_trans (sub1G _); rewrite -tiUV !subsetI subsetIl subIset ?sVE //=. rewrite -(pmaxElem_LdivP p_pr maxF) -defF centM -!setIA -(setICA 'C(W)). rewrite setIC (setIA G) setIS // subsetI cUV sub_LdivT. by case/and3P: (abelemS sVE abelE). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(div fintype finfun bigop finset prime binomial) mathcomp(fingroup morphism perm automorphism quotient) mathcomp(action commutator gproduct gfunctor ssralg) mathcomp(countalg finalg zmodp cyclic pgroup center gseries) mathcomp(nilpotent sylow abelian finmodule)