proposition: Lemma DnQ_extraspecial n : extraspecial 'D^n*Q.
proof: Proof. case: DnQ_P (DnQ_pgroup n) => gz isoZ pDnQ. have [injDn injQ] := (injm_cpairg1 isoZ, injm_cpair1g isoZ). have [n0 | n_gt0] := posnP n. rewrite -im_cpair mulSGid; first exact: injm_extraspecial Q8_extraspecial. apply/setIidPl; rewrite setI_im_cpair -injm_center //=. by congr (_ @* _); rewrite n0 center_ncprod0. apply: (cprod_extraspecial pDnQ (im_cpair_cprod isoZ) (setI_im_cpair _)). exact: injm_extraspecial (pX1p2n_extraspecial _ _). exact: injm_extraspecial Q8_extraspecial. 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)