proposition: Lemma normal_MXn_2 (p : {poly R}) (n : nat) : p * 'X^n \is normal -> p \is normal.
proof: Proof. elim : n => [| n Hn H]. by rewrite expr0 mulr1. rewrite exprSr mulrA in H. by rewrite Hn // normal_MX_2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path choice fintype order) mathcomp(prime div bigop ssralg poly polydiv polyorder ssrnum zmodp) mathcomp(polyrcf qe_rcf_th complex)