proposition: Lemma rank_DnQ n : 'r_2('D^n*Q) = n.+1.
proof: Proof. have pDnQ: 2.-group 'D^n*Q := DnQ_pgroup n. have esDnQ: extraspecial 'D^n*Q := DnQ_extraspecial n. do [case: DnQ_P => gz isoZ; set DnQ := setT] in pDnQ esDnQ *. suffices [E]: exists2 E, E \in 'E*_2(DnQ) & logn 2 #|E| = n.+1. by rewrite (pmaxElem_extraspecial pDnQ esDnQ); case/pnElemP=> _ _ <-. have oZ: #|'Z(DnQ)| = 2 by apply: card_center_extraspecial. pose Dn := cpairg1 isoZ @* 'D^n; pose Q := cpair1g isoZ @* 'Q_8. have [injDn injQ] := (injm_cpairg1 isoZ, injm_cpair1g isoZ). have [E EprE]:= p_rank_witness 2 [group of Dn]. have [sEDn abelE dimE] := pnElemP EprE; have [pE cEE eE]:= and3P abelE. rewrite injm_p_rank // rank_Dn in dimE; exists E => //. have sZE: 'Z(DnQ) \subset E. have maxE := subsetP (p_rankElem_max _ _) E EprE. have abelZ: 2.-abelem 'Z(DnQ) by rewrite prime_abelem ?oZ. rewrite -(Ohm1_id abelZ) (OhmE _ (abelem_pgroup abelZ)) gen_subG. rewrite -(pmaxElem_LdivP _ maxE) // setSI //=. by rewrite -cpairg1_center injm_center // setIS ?centS. have scE: 'C_Dn(E) = E. apply/eqP; rewrite eq_sym eqEcard subsetI sEDn -abelianE cEE /=. have [n0 | n_gt0] := posnP n. rewrite subset_leq_card // subIset // (subset_trans _ sZE) //. by rewrite -cpairg1_center morphimS // n0 center_ncprod0. have pDn: 2.-group Dn by rewrite morphim_pgroup ?pX1p2n_pgroup. have esDn: extraspecial Dn. exact: injm_extraspecial (pX1p2n_extraspecial _ _). rewrite dvdn_leq ?cardG_gt0 // (card_subcent_extraspecial pDn) //=. rewrite -injm_center // cpairg1_center (setIidPl sZE) oZ. rewrite -(dvdn_pmul2l (cardG_gt0 E)) mulnn mulnCA Lagrange //. rewrite card_injm ?card_pX1p2n // -expnS pfactor_dvdn ?expn_gt0 ?cardG_gt0 //. by rewrite lognX dimE mul2n. apply/pmaxElemP; split=> [|F E2F sEF]; first by rewrite inE subsetT abelE. have{E2F} [_ abelF] := pElemP E2F; have [pF cFF eF] := and3P abelF. apply/eqP; rewrite eqEsubset sEF andbT; apply/subsetP=> x Fx. have DnQx: x \in Dn * Q by rewrite im_cpair inE. have{DnQx} [y z Dn_y Qz def_x]:= imset2P DnQx. have{Dn_y} Ey: y \in E. have cEz: z \in 'C(E). by rewrite (subsetP (centS sEDn)) // (subsetP (im_cpair_cent _)). rewrite -scE inE Dn_y -(groupMr _ cEz) -def_x (subsetP (centS sEF)) //. by rewrite (subsetP cFF). rewrite def_x groupMl // (subsetP sZE) // -cpair1g_center injm_center //= -/Q. have: z \in 'Ohm_1(Q). rewrite (OhmE 1 (pgroupS (subsetT Q) pDnQ)) mem_gen // !inE Qz /=. rewrite -[z](mulKg y) -def_x (exponentP eF) ?groupM //. by rewrite groupV (subsetP sEF). have isoQ: Q \isog 'Q_(2 ^ 3) by rewrite isog_sym sub_isog. have [//|[u v] genQ _] := generators_quaternion _ isoQ. by case/quaternion_structure: genQ => // _ _ [-> _ _ [-> _] _] _ _. 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)