proposition: Lemma pX1p2n_extraspecial n : prime p -> n > 0 -> extraspecial p^{1+2*n}.
proof: Proof. move=> p_pr; elim: n => [//|n IHn _]. have esG := pX1p2_extraspecial p_pr. have [n0 | n_gt0] := posnP n. by apply: isog_extraspecial esG; rewrite isog_sym n0 pX1p2id. case: pX1p2S (pX1p2n_pgroup n.+1 p_pr) => gz isoZ pGn. apply: (cprod_extraspecial pGn (im_cpair_cprod isoZ) (setI_im_cpair isoZ)). by apply: injm_extraspecial esG; rewrite ?injm_cpairg1. by apply: injm_extraspecial (IHn n_gt0); rewrite ?injm_cpair1g. 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)