proposition: Lemma normal_MX (p : {poly R}) : p \is normal -> p * 'X \is normal.
proof: Proof. move=> Hpnormal. have Hpneq0 := (normal_neq0 Hpnormal). case : p Hpneq0 Hpnormal => s Hs. rewrite !normalE /= => Hp Hsnormal. rewrite polyseqMX //=. case : s Hs Hp Hsnormal => // a. case => [Hs Hp Ha | b l]. by apply/andP. elim: l a b => [b c Hs Hp Hab | c l Hcl a b Hs Hp Habcl]; apply/andP; split => //; apply/orP; by left. 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)