proposition: Lemma min_card_extraspecial : #|S| >= p ^ 3.
proof: Proof. have p_gt1 := prime_gt1 extraspecial_prime. rewrite leqNgt (card_pgroup pS) ltn_exp2l // ltnS. case: esS => [[_ defS']]; apply: contraL => /(p2group_abelian pS)/derG1P S'1. by rewrite -defS' S'1 cards1. 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)