proposition: Lemma exponent_2extraspecial G : 2.-group G -> extraspecial G -> exponent G = 4.
proof: Proof. move=> p2G esG; have [spG _] := esG. case/dvdn_pfactor: (exponent_special p2G spG) => // k. rewrite leq_eqVlt ltnS => /predU1P[-> // | lek1] expG. case/negP: (extraspecial_nonabelian esG). by rewrite (@abelem_abelian _ 2) ?exponent2_abelem // expG pfactor_dvdn. 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)