proposition: Lemma normal_MX_2 (p : {poly R}) : p * 'X \is normal -> p \is normal.
proof: Proof. move=> HpXnormal. have HpXneq0 := normal_neq0 HpXnormal. have Hpneq0 : p != 0 by rewrite -lead_coef_eq0 -lead_coefMX lead_coef_eq0. case : p Hpneq0 HpXneq0 HpXnormal => s Hs. rewrite !normalE /= => Hp HpX Hsnormal. rewrite polyseqMX // in Hsnormal. case : s Hs Hp HpX Hsnormal => [Hs Hp HpX H /= | a]. by rewrite /= ltxx in H. case => [Hs Hp HpX Ha /=| b l]. by rewrite /= lexx /= in Ha. elim: l a b => [b c Hs Hp HpX /andP Hab /= | c l Hcl a b Hs Hp HpX /andP Habcl]. exact: proj1 Hab. exact: proj1 Habcl. 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)