proposition: Lemma normal_red_0noroot : forall (p : {poly R}), p \is normal -> root p 0 -> ~~(root (p %/ 'X^(\mu_0 p)) 0) && ((p %/ 'X^(\mu_0 p)) \is normal).
proof: Proof. move=> p Hpnormal Hproot0. have Hpneq0 := (normal_neq0 Hpnormal). apply/andP; split. rewrite -(@addr0 _ 'X) -oppr0 -mu_gt0. by rewrite -eqn0Ngt (@mu_div _ _ _ (\mu_0 p)) //= subnn. rewrite divpN0. by rewrite dvdp_leq // ?root_mu. by rewrite -size_poly_gt0 size_exp_XsubC. have Hcoefs : forall k, ((p %/ 'X^(\mu_0 p))`_k = p`_(k + (\mu_0 p))). have H := (root_mu p 0). rewrite oppr0 addr0 Pdiv.IdomainMonic.dvdp_eq in H. rewrite {3}(eqP H) => k {H}; rewrite coefMXn /=. have H : ((k + \mu_0 p < \mu_0 p)%N = false). by rewrite -{2}(add0n (\mu_0 p)) (@ltn_add2r). by rewrite H addnK. by apply: monicXn. have Hsize : ((size (p %/ ('X^(\mu_0 p)))) = ((size p) - (\mu_0 p))%N). rewrite size_divp. by rewrite size_polyXn -pred_Sn. by rewrite -size_poly_gt0 size_polyXn ltn0Sn. have/normalP [Hp1 Hp2 Hp3 Hp4] := Hpnormal. apply/normalP; split => [k | |k Hk |i ]. + by rewrite Hcoefs Hp1. + rewrite lead_coefE Hcoefs Hsize -subnS addnC addnBA. by rewrite addnC subnS addnK Hp2. by rewrite -(size_polyXn R (\mu_0 p)) dvdp_leq // -(addr0 'X) -oppr0 root_mu. + by rewrite !Hcoefs (@addnC k.+1) addnS (@addnC k.-1) (@addnC k) -subn1 addnBA // subn1 Hp3 // (ltn_trans Hk) // -{1}(add0n k) ltn_add2r mu_gt0. rewrite Hcoefs => Hi j Hj1; rewrite Hsize => Hj2; rewrite Hcoefs (@Hp4 (i + (\mu_0 p))%N) // ?ltn_add2r //. by rewrite addnC -ltn_subRL -subn1 -subnDA addnC addn1 subnS. 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)