proposition: Lemma DnQ_P n : xcprod_spec 'D^n 'Q_8 ('D^n*Q)%type.
proof: Proof. have pQ: 2.-group 'Q_(2 ^ 3) by rewrite /pgroup card_quaternion. have{pQ} oZQ := card_center_extraspecial pQ Q8_extraspecial. suffices oZDn: #|'Z('D^n)| = 2. by apply: xcprodP; rewrite isog_cyclic_card ?prime_cyclic ?oZQ ?oZDn. have [-> | n_gt0] := posnP n; first by rewrite center_ncprod0 card_pX1p2n. have pr2: prime 2 by []; have pDn := pX1p2n_pgroup n pr2. exact: card_center_extraspecial (pX1p2n_extraspecial pr2 n_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)