proposition: Lemma p3group_extraspecial G : p.-group G -> ~~ abelian G -> logn p #|G| <= 3 -> extraspecial G.
proof: Proof. move=> pG not_cGG; have /andP[sZG nZG] := center_normal G. have ntG: G :!=: 1 by apply: contraNneq not_cGG => ->; apply: abelian1. have ntZ: 'Z(G) != 1 by rewrite (center_nil_eq1 (pgroup_nil pG)). have [p_pr _ [n oG]] := pgroup_pdiv pG ntG; rewrite oG pfactorK //. have [_ _ [m oZ]] := pgroup_pdiv (pgroupS sZG pG) ntZ. have lt_m1_n: m.+1 < n. suffices: 1 < logn p #|(G / 'Z(G))|. rewrite card_quotient // -divgS // logn_div ?cardSg //. by rewrite oG oZ !pfactorK // ltn_subRL addn1. rewrite ltnNge; apply: contra not_cGG => cycGs. apply: cyclic_center_factor_abelian; rewrite (dvdn_prime_cyclic p_pr) //. by rewrite (card_pgroup (quotient_pgroup _ pG)) (dvdn_exp2l _ cycGs). rewrite -{lt_m1_n}(subnKC lt_m1_n) !addSn !ltnS leqn0 in oG *. case: m => // in oZ oG * => /eqP n2; rewrite {n}n2 in oG. exact: card_p3group_extraspecial oZ. 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)