proposition: Lemma card_DnQ n : #|'D^n*Q| = (2 ^ n.+1.*2.+1)%N.
proof: Proof. have oQ: #|'Q_(2 ^ 3)| = 8 by rewrite card_quaternion. have pQ: 2.-group 'Q_8 by rewrite /pgroup oQ. case: DnQ_P => gz isoZ. rewrite -im_cpair cardMg_divn setI_im_cpair cpair_center_id. rewrite -injm_center 3?{1}card_injm ?injm_cpairg1 ?injm_cpair1g ?center_sub //. rewrite oQ card_pX1p2n // (card_center_extraspecial pQ Q8_extraspecial). by rewrite -muln_divA // mulnC -(expnD 2 2). 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)