proposition: Lemma card_p3group_extraspecial E : prime p -> #|E| = (p ^ 3)%N -> #|'Z(E)| = p -> extraspecial E.
proof: Proof. move=> p_pr oEp3 oZp; have p_gt0 := prime_gt0 p_pr. have pE: p.-group E by rewrite /pgroup oEp3 pnatX pnat_id. have pEq: p.-group (E / 'Z(E))%g by rewrite quotient_pgroup. have /andP[sZE nZE] := center_normal E. have oEq: #|E / 'Z(E)|%g = (p ^ 2)%N. by rewrite card_quotient -?divgS // oEp3 oZp expnS mulKn. have cEEq: abelian (E / 'Z(E))%g by apply: card_p2group_abelian oEq. have not_cEE: ~~ abelian E. have: #|'Z(E)| < #|E| by rewrite oEp3 oZp (ltn_exp2l 1) ?prime_gt1. by apply: contraL => cEE; rewrite -leqNgt subset_leq_card // subsetI subxx. have defE': E^`(1) = 'Z(E). apply/eqP; rewrite eqEsubset der1_min //=; apply: contraR not_cEE => not_sE'Z. apply/commG1P/(TI_center_nil (pgroup_nil pE) (der_normal 1 _)). by rewrite setIC prime_TIg ?oZp. split; [split=> // | by rewrite oZp]; apply/eqP. rewrite eqEsubset andbC -{1}defE' {1}(Phi_joing pE) joing_subl. rewrite -quotient_sub1 ?gFsub_trans ?subG1 //=. rewrite (quotient_Phi pE) //= (trivg_Phi pEq). apply/abelemP=> //; split=> // Zx EqZx; apply/eqP; rewrite -order_dvdn /order. rewrite (card_pgroup (mem_p_elt pEq EqZx)) (@dvdn_exp2l _ _ 1) //. rewrite leqNgt -pfactor_dvdn // -oEq; apply: contra not_cEE => sEqZx. rewrite cyclic_center_factor_abelian //; apply/cyclicP. exists Zx; apply/eqP; rewrite eq_sym eqEcard cycle_subG EqZx -orderE. exact: dvdn_leq sEqZx. 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)