proposition: Lemma exponent_special : p.-group G -> special G -> exponent G %| p ^ 2.
proof: Proof. move=> pG spG; have [defPhi _] := spG. have /and3P[_ _ expZ] := center_special_abelem pG spG. apply/exponentP=> x Gx; rewrite expgM (exponentP expZ) // -defPhi. by rewrite (Phi_joing pG) mem_gen // inE orbC (Mho_p_elt 1) ?(mem_p_elt pG). 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)