proposition: Lemma pX1p2_extraspecial : extraspecial p^{1+2}.
proof: Proof. apply: (p3group_extraspecial pX1p2_pgroup); last first. by rewrite card_pX1p2 pfactorK. case/existsP: (isoGrp_hom Grp_pX1p2) card_pX1p2 => [[x y]] /=. case/eqP=> <- xp yp _ _ oXY. apply: contraL (dvdn_cardMg <[x]> <[y]>) => cXY_XY. rewrite -cent_joinEl ?(sub_abelian_cent2 cXY_XY) ?joing_subl ?joing_subr //. rewrite oXY -!orderE pfactor_dvdn ?muln_gt0 ?order_gt0 // -leqNgt. rewrite -(pfactorK 2 p_pr) dvdn_leq_log ?expn_gt0 ?p_gt0 //. by rewrite dvdn_mul ?order_dvdn ?xp ?yp. 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)