proposition: Lemma isog_pX1p2n n (gT : finGroupType) (G : {group gT}) : prime p -> extraspecial G -> #|G| = (p ^ n.*2.+1)%N -> exponent G %| p -> G \isog p^{1+2*n}.
proof: Proof. move=> p_pr esG oG expG; have p_gt1 := prime_gt1 p_pr. have not_le_p3_p: ~~ (p ^ 3 <= p) by rewrite (leq_exp2l 3 1). have pG: p.-group G by rewrite /pgroup oG pnatX pnat_id. have oZ := card_center_extraspecial pG esG. have{pG esG} [Es p3Es defG] := extraspecial_structure pG esG. set Z := 'Z(G) in oZ defG p3Es. elim: Es {+}G => [|E Es IHs] S in n oG expG p3Es defG *. rewrite big_nil cprod1g in defG; rewrite -defG. have ->: n = 0. apply: double_inj; apply/eqP. by rewrite -eqSS -(eqn_exp2l _ _ p_gt1) -oG -defG oZ. by rewrite isog_cyclic_card prime_cyclic ?oZ ?card_pX1p2n //=. rewrite big_cons -cprodA in defG; rewrite /= -andbA in p3Es. have [[_ T _ defT] defET cTE] := cprodP defG; rewrite defT in defET cTE defG. move: p3Es => /and3P[/eqP oE /eqP defZE /IHs{}IHs]. have not_cEE: ~~ abelian E. by apply: contra not_le_p3_p => cEE; rewrite -oE -oZ -defZE (center_idP _). have sES: E \subset S by rewrite -defET mulG_subl. have sTS: T \subset S by rewrite -defET mulG_subr. have expE: exponent E %| p by apply: dvdn_trans (exponentS sES) expG. have expT: exponent T %| p by apply: dvdn_trans (exponentS sTS) expG. have{expE not_cEE} isoE: E \isog p^{1+2}. apply: isog_pX1p2 => //. by apply: card_p3group_extraspecial p_pr oE _; rewrite defZE. have sZT: 'Z(E) \subset T. by case/cprodP: defT => [[U _ -> _] <- _]; rewrite defZE mulG_subr. case def_n: n => [|n']. case/negP: not_le_p3_p; rewrite def_n in oG; rewrite -oE -[p]oG. exact: subset_leq_card. have zI_ET: E :&: T = 'Z(E). by apply/eqP; rewrite eqEsubset subsetI sZT subsetIl setIS // centsC. have{n def_n oG} oT: #|T| = (p ^ n'.*2.+1)%N. apply/eqP; rewrite -(eqn_pmul2l (cardG_gt0 E)) mul_cardG zI_ET defET. by rewrite defZE oE oG oZ -expnSr -expnD def_n. have{IHs oT expT defT Es} isoT: T \isog p^{1+2*n'} by rewrite IHs. case: pX1p2S => gz isoZ; rewrite (isog_cprod_by _ defG) //. exact: Aut_extraspecial_full (pX1p2_pgroup p_pr) (pX1p2_extraspecial p_pr). 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)