proposition: Lemma rank_Dn n : 'r_2('D^n) = n.+1.
proof: Proof. elim: n => [|n IHn]; first by rewrite p_rank_abelem ?prime_abelem ?card_pX1p2n. have oDDn: #|'D^n.+1| = (2 ^ n.+1.*2.+1)%N by apply: card_pX1p2n. have esDDn: extraspecial 'D^n.+1 by apply: pX1p2n_extraspecial. do [case: pX1p2S => gz isoZ; set DDn := [set: _]] in oDDn esDDn *. have pDDn: 2.-group DDn by rewrite /pgroup oDDn pnatX. apply/eqP; rewrite eqn_leq; apply/andP; split. have [E EprE]:= p_rank_witness 2 [group of DDn]. have [sEDDn abelE <-] := pnElemP EprE; have [pE cEE _]:= and3P abelE. rewrite -(@leq_exp2l 2) // -p_part part_pnat_id // -leq_sqr -expnM -mulnn. rewrite muln2 doubleS expnS -oDDn -(@leq_pmul2r #|'C_DDn(E)|) ?cardG_gt0 //. rewrite {1}(card_subcent_extraspecial pDDn) // mulnCA -mulnA Lagrange //=. rewrite mulnAC mulnA leq_pmul2r ?cardG_gt0 // setTI. have ->: (2 * #|'C(E)| = #|'Z(DDn)| * #|'C(E)|)%N. by rewrite (card_center_extraspecial pDDn). by rewrite leq_mul ?subset_leq_card ?subsetIl. have [inj1 injn] := (injm_cpairg1 isoZ, injm_cpair1g isoZ). pose D := cpairg1 isoZ @* 2^{1+2}; pose Dn := cpair1g isoZ @* 'D^n. have [E EprE] := p_rank_witness 2 [group of Dn]. rewrite injm_p_rank //= IHn in EprE; have [sEDn abelE dimE]:= pnElemP EprE. have [x [Dx ox] notDnx]: exists x, [/\ x \in D, #[x] = 2 & x \notin Dn]. have isoD: D \isog 'D_(2 ^ 3). by rewrite isog_sym -(isog_transl _ isog_2X1p2) sub_isog. have [//| [x y] genD [oy _]] := generators_2dihedral _ isoD. have [_ _ _ X'y] := genD; case/setDP: X'y; rewrite /= -/D => Dy notXy. exists y; split=> //; apply: contra notXy => Dny. case/dihedral2_structure: genD => // _ _ _ _ [defZD _ _ _ _]. by rewrite (subsetP (cycleX x 2)) // -defZD -setI_im_cpair inE Dy. have def_xE: <[x]> \x E = <[x]> <*> E. rewrite dprodEY ?prime_TIg -?orderE ?ox //. by rewrite (centSS sEDn _ (im_cpair_cent _)) ?cycle_subG. by rewrite cycle_subG (contra (subsetP sEDn x)). apply/p_rank_geP; exists (<[x]> <*> E)%G. rewrite 2!inE subsetT (dprod_abelem _ def_xE) abelE -(dprod_card def_xE). by rewrite prime_abelem -?orderE ?ox //= lognM ?cardG_gt0 ?dimE. 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)