proposition: Lemma card_pX1p2n n : prime p -> #|p^{1+2*n}| = (p ^ n.*2.+1)%N.
proof: Proof. move=> p_pr; have pG := pX1p2_pgroup p_pr. have oG := card_pX1p2 p_pr; have esG := pX1p2_extraspecial p_pr. have oZ := card_center_extraspecial pG esG. elim: n => [|n IHn]; first by rewrite (card_isog (ncprod0 _)) oZ. case: pX1p2S => gz isoZ; rewrite -im_cpair cardMg_divn setI_im_cpair. rewrite -injm_center ?{1}card_injm ?injm_cpairg1 ?injm_cpair1g ?center_sub //. by rewrite oG oZ IHn -expnD mulKn ?prime_gt0. 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)