proposition: Theorem extraspecial_structure S : p.-group S -> extraspecial S -> {Es | all (fun E => (#|E| == p ^ 3)%N && ('Z(E) == 'Z(S))) Es & \big[cprod/1%g]_(E <- Es) E \* 'Z(S) = S}.
proof: Proof. have [m] := ubnP #|S|; elim: m S => // m IHm S leSm pS esS. have [x Z'x]: {x | x \in S :\: 'Z(S)}. apply/sigW/set0Pn; rewrite -subset0 subDset setU0. apply: contra (extraspecial_nonabelian esS) => sSZ. exact: abelianS sSZ (center_abelian S). have [E [R [[oE oR]]]]:= split1_extraspecial pS esS Z'x. case=> defS _ [defZE defZR] _; case: ifP => [_ defR | _ esR]. by exists [:: E]; rewrite /= ?oE ?defZE ?eqxx // big_seq1 -defR. have sRS: R \subset S by case/cprodP: defS => _ <- _; rewrite mulG_subr. have [|Es esEs defR] := IHm _ _ (pgroupS sRS pS) esR. rewrite oR (leq_trans (ltn_Pdiv _ _)) ?cardG_gt0 // (ltn_exp2l 0) //. exact: prime_gt1 (extraspecial_prime pS esS). exists (E :: Es); first by rewrite /= oE defZE !eqxx -defZR. by rewrite -defZR big_cons -cprodA defR. 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)