proposition: Lemma isog_pX1p2 (gT : finGroupType) (G : {group gT}) : extraspecial G -> exponent G %| p -> #|G| = (p ^ 3)%N -> G \isog p^{1+2}.
proof: Proof. move=> esG expGp oG; apply/(isoGrpP _ Grp_pX1p2). rewrite card_pX1p2; split=> //. have pG: p.-group G by rewrite /pgroup oG pnatX pnat_id. have oZ := card_center_extraspecial pG esG. have [x Gx notZx]: exists2 x, x \in G & x \notin 'Z(G). apply/subsetPn; rewrite proper_subn // properEcard center_sub oZ oG. by rewrite (ltn_exp2l 1 3). have ox: #[x] = p. by apply: nt_prime_order; rewrite ?(exponentP expGp) ?(group1_contra notZx). have [y Gy not_cxy]: exists2 y, y \in G & y \notin 'C[x]. by apply/subsetPn; rewrite sub_cent1; rewrite inE Gx in notZx. apply/existsP; exists (x, y) => /=; set z := [~ x, y]. have [[defPhiG defG'] _] := esG. have Zz: z \in 'Z(G) by rewrite -defG' mem_commg. have [Gz cGz] := setIP Zz; rewrite !xpair_eqE !(exponentP expGp) //. have [_ nZG] := andP (center_normal G). rewrite /commg /conjg !(centP cGz) // !mulKg mulVg !eqxx !andbT. have sXY_G: <[x]> <*> <[y]> \subset G by rewrite join_subG !cycle_subG Gx. have defZ: <[z]> = 'Z(G). apply/eqP; rewrite eqEcard cycle_subG Zz oZ /= -orderE. rewrite (nt_prime_order p_pr) ?(exponentP expGp) //. by rewrite (sameP commgP cent1P) cent1C. have sZ_XY: 'Z(G) \subset <[x]> <*> <[y]>. by rewrite -defZ cycle_subG groupR // mem_gen // inE cycle_id ?orbT. rewrite eqEcard sXY_G /= oG -(Lagrange sZ_XY) oZ leq_pmul2l //. rewrite -card_quotient ?(subset_trans sXY_G) //. rewrite quotientY ?quotient_cycle ?cycle_subG ?(subsetP nZG) //. have abelGz: p.-abelem (G / 'Z(G)) by rewrite -defPhiG Phi_quotient_abelem. have [cGzGz expGz] := abelemP p_pr abelGz. rewrite cent_joinEr ?(sub_abelian_cent2 cGzGz) ?cycle_subG ?mem_quotient //. have oZx: #|<[coset 'Z(G) x]>| = p. rewrite -orderE (nt_prime_order p_pr) ?expGz ?mem_quotient //. by apply: contra notZx; move/eqP=> Zx; rewrite coset_idr ?(subsetP nZG). rewrite TI_cardMg ?oZx -?orderE ?(nt_prime_order p_pr) ?expGz ?mem_quotient //. apply: contra not_cxy; move/eqP=> Zy. rewrite -cent_cycle (subsetP _ y (coset_idr _ Zy)) ?(subsetP nZG) //. by rewrite subIset ?centS ?orbT ?cycle_subG. rewrite prime_TIg ?oZx // cycle_subG; apply: contra not_cxy. case/cycleP=> i; rewrite -morphX ?(subsetP nZG) // => /rcoset_kercosetP. rewrite groupX ?(subsetP nZG) // cent1C => /(_ isT isT); apply: subsetP. rewrite mul_subG ?sub1set ?groupX ?cent1id //= -cent_cycle subIset // orbC. by rewrite centS ?cycle_subG. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset prime binomial) mathcomp(fingroup morphism perm automorphism presentation) mathcomp(quotient action commutator gproduct gfunctor) mathcomp(ssralg finalg zmodp cyclic pgroup center gseries) mathcomp(nilpotent sylow abelian finmodule matrix maximal) mathcomp(extremal)