proposition: Lemma exponent_pX1p2 : odd p -> exponent p^{1+2} %| p.
proof: Proof. move=> p_odd; have pG := pX1p2_pgroup. have ->: p^{1+2} = 'Ohm_1(p^{1+2}). apply/eqP; rewrite eqEsubset Ohm_sub andbT (OhmE 1 pG). case/existsP: (isoGrp_hom Grp_pX1p2) => [[x y]] /=. case/eqP=> <- xp yp _ _; rewrite joing_idl joing_idr genS //. by rewrite subsetI subset_gen subUset !sub1set !inE xp yp!eqxx. rewrite exponent_Ohm1_class2 ?card_pX1p2 ?oddX // nil_class2. by have [[_ ->] _ ] := pX1p2_extraspecial. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset prime binomial) mathcomp(fingroup morphism perm automorphism presentation) mathcomp(quotient action commutator gproduct gfunctor) mathcomp(ssralg finalg zmodp cyclic pgroup center gseries) mathcomp(nilpotent sylow abelian finmodule matrix maximal) mathcomp(extremal)