proposition: Lemma normal_mulr : forall p q : {poly R}, p \is normal -> q \is normal -> (p * q) \is normal.
proof: Proof. move=> p q Hpnormal Hqnormal. have Hp0 := (root_mu p 0). have Hq0 := (root_mu q 0). rewrite Pdiv.Field.dvdp_eq in Hp0. rewrite Pdiv.Field.dvdp_eq in Hq0. have Hp0notroot1 : (~~(root (p %/ ('X - 0%:P) ^+ \mu_0 p) 0) ). rewrite -mu_gt0 ?mu_div //. by rewrite (addnK (\mu_0 p) 0%N) ltnn. by rewrite dvdp_div_eq0 ?normal_neq0 // root_mu. have Hq0notroot1 : (~~(root (q %/ ('X - 0%:P) ^+ \mu_0 q) 0) ). rewrite -mu_gt0 ?mu_div //. by rewrite (addnK (\mu_0 q) 0%N) ltnn. by rewrite dvdp_div_eq0 ?normal_neq0 // root_mu. rewrite (eqP Hp0) (eqP Hq0) [x in (x * _)]mulrC !mulrA (mulrC _ (('X - 0%:P) ^+ \mu_0 q)) !mulrA -exprD {1}oppr0 addr0 -mulrA mulrC normal_MXn //. apply: normal_mulr_r => //. rewrite (eqP Hp0) {2}oppr0 addr0 in Hpnormal. by apply: (normal_MXn_2 (n:=\mu_0 p)). rewrite (eqP Hq0) {2}oppr0 addr0 in Hqnormal. by apply: (normal_MXn_2 (n:=\mu_0 q)). 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)