proposition: Lemma card_extraspecial : {n | n > 0 & #|S| = (p ^ n.*2.+1)%N}.
proof: Proof. set T := S; exists (logn p #|T|)./2. rewrite half_gt0 ltnW // -(leq_exp2l _ _ (prime_gt1 p_pr)) -card_pgroup //. exact: min_card_extraspecial. have [Es] := extraspecial_structure pS esS; rewrite -[in RHS]/T. elim: Es T => [_ _ <-| E s IHs T] /=. by rewrite big_nil cprod1g oZ (pfactorK 1). rewrite -andbA big_cons -cprodA => /and3P[/eqP oEp3 /eqP defZE]. move=> /IHs{}IHs /cprodP[[_ U _ defU]]; rewrite defU => defT cEU. rewrite -(mulnK #|T| (cardG_gt0 (E :&: U))) -defT -mul_cardG /=. have ->: E :&: U = 'Z(S). apply/eqP; rewrite eqEsubset subsetI -{1 2}defZE subsetIl setIS //=. by case/cprodP: defU => [[V _ -> _]] <- _; apply: mulG_subr. rewrite (IHs U) // oEp3 oZ -expnD addSn expnS mulKn ?prime_gt0 //. by rewrite pfactorK //= uphalf_double. 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)