proposition: Lemma not_isog_Dn_DnQ n : ~~ ('D^n \isog 'D^n.-1*Q).
proof: Proof. case: n => [|n] /=; first by rewrite isogEcard card_pX1p2n // card_DnQ andbF. apply: contraL (leqnn n.+1) => isoDn1DnQ. by rewrite -ltnNge -rank_Dn (isog_p_rank isoDn1DnQ) rank_DnQ. 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)