proposition: Lemma split1_extraspecial x : x \in G :\: 'Z(G) -> {E : {group gT} & {R : {group gT} | [/\ #|E| = (p ^ 3)%N /\ #|R| = #|G| %/ p ^ 2, E \* R = G /\ E :&: R = 'Z(E), 'Z(E) = 'Z(G) /\ 'Z(R) = 'Z(G), extraspecial E /\ x \in E & if abelian R then R :=: 'Z(G) else extraspecial R]}}.
proof: Proof. case/setDP=> Gx notZx; rewrite inE Gx /= in notZx. have [[defPhiG defG'] prZ] := esG. have maxCx: maximal 'C_G[x] G. by rewrite subcent1_extraspecial_maximal // inE notZx. pose y := repr (G :\: 'C[x]). have [Gy not_cxy]: y \in G /\ y \notin 'C[x]. move/maxgroupp: maxCx => /properP[_ [t Gt not_cyt]]. by apply/setDP; apply: (mem_repr t); rewrite !inE Gt andbT in not_cyt *. pose E := <[x]> <*> <[y]>; pose R := 'C_G(E). exists [group of E]; exists [group of R] => /=. have sEG: E \subset G by rewrite join_subG !cycle_subG Gx. have [Ex Ey]: x \in E /\ y \in E by rewrite !mem_gen // inE cycle_id ?orbT. have sZE: 'Z(G) \subset E. rewrite (('Z(G) =P E^`(1)) _) ?der_sub // eqEsubset -{2}defG' dergS // andbT. apply: contraR not_cxy => /= not_sZE'. rewrite (sameP cent1P commgP) -in_set1 -[[set 1]](prime_TIg prZ not_sZE'). by rewrite /= -defG' inE !mem_commg. have ziER: E :&: R = 'Z(E) by rewrite setIA (setIidPl sEG). have cER: R \subset 'C(E) by rewrite subsetIr. have iCxG: #|G : 'C_G[x]| = p by apply: p_maximal_index. have maxR: maximal R 'C_G[x]. rewrite /R centY !cent_cycle setIA. rewrite subcent1_extraspecial_maximal ?subsetIl // inE Gy andbT -sub_cent1. by apply/subsetPn; exists x; rewrite 1?cent1C // inE Gx cent1id. have sRCx: R \subset 'C_G[x] by rewrite -cent_cycle setIS ?centS ?joing_subl. have sCxG: 'C_G[x] \subset G by rewrite subsetIl. have sRG: R \subset G by rewrite subsetIl. have iRCx: #|'C_G[x] : R| = p by rewrite (p_maximal_index (pgroupS sCxG pG)). have defG: E * R = G. rewrite -cent_joinEr //= -/R joingC joingA. have cGx_x: <[x]> \subset 'C_G[x] by rewrite cycle_subG inE Gx cent1id. have nsRcx := p_maximal_normal (pgroupS sCxG pG) maxR. rewrite (norm_joinEr (subset_trans cGx_x (normal_norm nsRcx))). rewrite (mulg_normal_maximal nsRcx) //=; last first. by rewrite centY !cent_cycle cycle_subG !in_setI Gx cent1id cent1C. have nsCxG := p_maximal_normal pG maxCx. have syG: <[y]> \subset G by rewrite cycle_subG. rewrite (norm_joinEr (subset_trans syG (normal_norm nsCxG))). by rewrite (mulg_normal_maximal nsCxG) //= cycle_subG inE Gy. have defZR: 'Z(R) = 'Z(G) by rewrite -['Z(R)]setIA -centM defG. have defZE: 'Z(E) = 'Z(G). by rewrite -defG -center_prod ?mulGSid //= -ziER subsetI center_sub defZR sZE. have [n oG] := p_natP pG. have n_gt1: n > 1. by rewrite ltnW // -(@leq_exp2l p) // -oG min_card_extraspecial. have oR: #|R| = (p ^ n.-2)%N. apply/eqP; rewrite -(divg_indexS sRCx) iRCx /= -(divg_indexS sCxG) iCxG /= oG. by rewrite -{1}(subnKC n_gt1) subn2 !expnS !mulKn. have oE: #|E| = (p ^ 3)%N. apply/eqP; rewrite -(@eqn_pmul2r #|R|) ?cardG_gt0 // mul_cardG defG ziER. by rewrite defZE oZ oG -{1}(subnKC n_gt1) oR -expnSr -expnD subn2. rewrite cprodE // oR oG -expnB ?subn2 //; split=> //. by split=> //; apply: card_p3group_extraspecial _ oE _; rewrite // defZE. case: ifP => [cRR | not_cRR]; first by rewrite -defZR (center_idP _). split; rewrite /special defZR //. have ntR': R^`(1) != 1 by rewrite (sameP eqP commG1P) -abelianE not_cRR. have pR: p.-group R := pgroupS sRG pG. have pR': p.-group R^`(1) := pgroupS (der_sub 1 _) pR. have defR': R^`(1) = 'Z(G). apply/eqP; rewrite eqEcard -{1}defG' dergS //= oZ. by have [_ _ [k ->]]:= pgroup_pdiv pR' ntR'; rewrite (leq_exp2l 1). split=> //; apply/eqP; rewrite eqEsubset -{1}defPhiG -defR' (PhiS pG) //=. by rewrite (Phi_joing pR) joing_subl. 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)