proposition: Lemma normal_mulr_r (p q : {poly R}) : ~~ root p 0 -> ~~ root q 0 -> p \is normal -> q \is normal -> (p * q) \is normal.
proof: Proof. move=> Hpzero Hqzero Hpnormal Hqnormal. apply/normalP; split=> [k | |k Hk |i Hpqi j Hij Hj]. have/normalP [Hp _ _ _] := Hpnormal. have/normalP [Hq _ _ _] := Hqnormal. rewrite coefM sumr_ge0 // => [i _] /=. by apply: mulr_ge0. have/normalP [_ Hp _ _] := Hpnormal. have/normalP [_ Hq _ _] := Hqnormal. by rewrite lead_coefM pmulr_lgt0. rewrite -subr_ge0 !coefM prednK // expr2 !big_distrlr /=. rewrite -(big_mkord (fun i : nat => true) (fun i : nat => \sum_(j < k.+1) (p`_i * q`_(k - i) * (p`_j * q`_(k - j))))). rewrite -(big_mkord (fun i : nat => true) (fun i : nat => \sum_(j < k.+2) (p`_i * q`_(k.-1 - i) * (p`_j * q`_(k.+1 - j))))). rewrite (eq_bigr (fun i => \sum_(0 <= j < k.+1) p`_i * q`_(k - i) * (p`_j * q`_(k - j)))); last by move => ? _ ; rewrite big_mkord. rewrite [x in _ - x](eq_bigr (fun i => \sum_(0 <= j < k.+2) p`_i * q`_(k.-1 - i) * (p`_j * q`_(k.+1 - j)))); last by move => ? _ ; rewrite big_mkord. have H : \sum_(0 <= i < k.+1) \sum_(0 <= j < k.+1) p`_i * q`_(k - i) * (p`_j * q`_(k - j)) = \sum_(2 <= h < k.+1) \sum_(0 <= j < h.-1) p`_h * q`_(k - h) * (p`_j * q`_(k - j)) + \sum_(1 <= h < k.+1) p`_h * q`_(k - h) * (p`_(h.-1) * q`_(k - h.-1)) + \sum_(0 <= h < k.+1) \sum_(h <= j < k.+1) p`_h * q`_(k - h) * (p`_j * q`_(k - j)). have H2: \sum_(0 <= i < k.+1) \sum_(0 <= j < k.+1) p`_i * q`_(k - i) * (p`_j * q`_(k - j)) = \sum_(0 <= i < k.+1) \sum_(0 <= j < i.-1) p`_i * q`_(k - i) * (p`_j * q`_(k - j)) + \sum_(0 <= i < k.+1) \sum_(i.-1 <= j < i) p`_i * q`_(k - i) * (p`_j * q`_(k - j)) + \sum_(0 <= i < k.+1) \sum_(i <= j < k.+1) p`_i * q`_(k - i) * (p`_j * q`_(k - j)). rewrite -big_split -big_split. rewrite big_nat [x in (_ = x)]big_nat; apply: eq_bigr => i Hi. rewrite -big_cat_nat //. rewrite -big_cat_nat //. apply: ltnW; by move/andP : Hi; case=> _ ->. by apply: leq_pred. rewrite H2 {H2}. congr (_ + _). rewrite big_nat_recl// big_geq ?add0r; last by apply: leq_pred. rewrite big_nat_recl// (big_geq (m:=0.-1) (n:=0)) // ?add0r. have H2 : \sum_(0 <= i < k) \sum_(i.+1.-1 <= j < i.+1) p`_i.+1 * q`_(k - i.+1) * (p`_j * q`_(k - j)) = \sum_(1 <= h < k.+1) p`_h * q`_(k - h) * (p`_h.-1 * q`_(k - h.-1)). rewrite big_add1 -pred_Sn big_nat [x in (_ = x)]big_nat. apply: eq_bigr=> i Hi. by rewrite -pred_Sn big_nat1. rewrite H2 {H2}. congr (_ + _). by rewrite -{1}(prednK Hk) big_nat_recl// big_geq // add0r big_add1 big_add1 -pred_Sn. rewrite H {H}. have H : \sum_(0 <= i < k) \sum_(0 <= j < k.+2) p`_i * q`_(k.-1 - i) * (p`_j * q`_(k.+1 - j)) = \sum_(0 <= h < k) \sum_(0 <= j < h.+1) p`_h * q`_(k.-1 - h) * (p`_j * q`_(k.+1 - j)) + \sum_(1 <= i < k.+1) p`_(i.-1) * q`_(k - i) * (p`_i * q`_(k.+1 - i)) + \sum_(0 <= h < k) \sum_(h.+2 <= j < k.+2) p`_h * q`_(k.-1 - h) * (p`_j * q`_(k.+1 - j)). rewrite big_add1 -pred_Sn -!big_split big_nat [x in (_ = x)]big_nat. apply: eq_bigr => h Hh. rewrite (big_cat_nat (n:= h.+1) (GRing.add_comoid R) (fun j => true) (fun j => p`_h * q`_(k.-1 - h) * (p`_j * q`_(k.+1 - j))) ) //. rewrite (big_cat_nat (n:= h.+2) (m:=h.+1) (GRing.add_comoid R) (fun j => true) (fun j => p`_h * q`_(k.-1 - h) * (p`_j * q`_(k.+1 - j))) ). rewrite big_nat1 -pred_Sn /= -/(nth 0 _ (h.+1)) !addrA. congr (_ + _); congr (_ + _). by rewrite -(addn1 h) (addnC h 1%N) (subnDA 1 k h) subn1. by rewrite (ltn_trans (n:=h.+1)) // ltnSn. case/andP: Hh => Hh1 Hh2. by rewrite (ltn_trans (n:=h.+2)) // ltnSn. by apply: (ltn_trans (n:=k)). rewrite H {H} [x in ((x + _) - _)]addrC -[x in (_ - x)]addrA [x in (_ - (_ + x))]addrC !opprD !addrA addrC -sumrN !addrA -big_split. have H : \big[GRing.add_comoid R/0]_(1 <= i < k.+1) (GRing.add_comoid R) (- (p`_i.-1 * q`_(k - i) * (p`_i * q`_(k.+1 - i)))) (p`_i * q`_(k - i) * (p`_i.-1 * q`_(k - i.-1))) = 0. rewrite big_split sumrN /= addrC. apply/eqP. rewrite subr_eq0. apply/eqP. rewrite big_nat [x in (_ = x)]big_nat. apply: eq_bigr => i Hi. rewrite mulrC -[x in (x = _)]mulrA [x in (_ * x = _)]mulrC [x in (_ * (x * _) = _)]mulrC !mulrA. congr (_ * _). rewrite -subn1 subnBA ?addn1 //. by case/andP : Hi. rewrite H {H} add0r big_add1 -pred_Sn. rewrite (eq_big (F1 := fun i => \sum_(0 <= j < i.+1.-1) p`_i.+1 * q`_(k - i.+1) * (p`_j * q`_(k - j))) (P1 := fun i => true) (fun i => true) (fun i => \sum_(1 <= l < i.+1) p`_i.+1 * q`_(k - i.+1) * (p`_(l.-1) * q`_(k - (l.-1))))) // =>[ | i _]. have H : \sum_(0 <= h < k) \sum_(h.+2 <= j < k.+2) p`_h * q`_(k.-1 - h) * (p`_j * q`_(k.+1 - j)) = \sum_(1 <= i < k.+1) \sum_(i <= l < k.+1) p`_i.-1 * q`_(k - i) * (p`_l.+1 * q`_(k - l)). rewrite big_add1 -pred_Sn. apply: eq_big_nat => i Hi. rewrite big_add1 -pred_Sn. apply: eq_big_nat => l Hl. by rewrite -pred_Sn subSS -(addn1 i) (addnC i 1%N) subnDA -subn1. rewrite H {H} xchange big_nat_recl//. have H : \sum_(0 <= i < k) \sum_(i.+1 <= j < k.+1) p`_i.+1 * q`_(k - i.+1) * (p`_j * q`_(k - j)) = \sum_(1 <= h < k.+1) \sum_(h <= j < k.+1) p`_h * q`_(k - h) * (p`_j * q`_(k - j)). by rewrite big_add1 -pred_Sn. rewrite H {H} [x in (_ + (_ + _) - x - _)]xchange -{12}(prednK Hk) [x in (_ + (_ + _) - x - _)]big_nat_recl//. have H :(\big[GRing.add_comoid R/0]_(0 <= i < k.-1) \big[GRing.add_comoid R/0]_(i.+1 <= j < k) (p`_j * q`_(k.-1 - j) * (p`_i.+1 * q`_(k.+1 - i.+1))) = \sum_(1 <= h < k) \sum_(h <= j < k) p`_h * q`_(k.+1 - h) * (p`_j * q`_(k.-1 - j))). rewrite big_add1 big_nat [x in (_ = x)]big_nat. apply: eq_bigr => i Hi. rewrite big_nat [x in (_ = x)]big_nat. apply: eq_bigr => j Hj. by rewrite mulrC. rewrite H {H}. have H : \sum_(1 <= i < k.+1) \sum_(i <= l < k.+1) p`_i.-1 * q`_(k - i) * (p`_l.+1 * q`_(k - l)) = \sum_(1 <= h < k) \sum_(h <= j < k) p`_h.-1 * q`_(k - h) * (p`_j.+1 * q`_(k - j)) + \sum_(1 <= i < k.+1) p`_i.-1 * q`_(k - i) * (p`_k.+1 * q`_0). rewrite (big_cat_nat (GRing.add_comoid R) (n:= k)) // big_nat1 big_nat1 [x in (_ = _ + x)](big_cat_nat (GRing.add_comoid R) (n:= k)) // big_nat1 (addnK k 0%N) Monoid.addmA. congr (_ + _). rewrite -big_split big_nat [x in (_ = x)]big_nat. apply: eq_bigr => i Hi. rewrite (big_cat_nat (GRing.add_comoid R) (n:= k)) //. rewrite big_nat1. by rewrite (addnK k 0%N). apply: ltnW. by case/andP : Hi. rewrite H {H}. have H : \sum_(1 <= h < k.+1) \sum_(h <= j < k.+1) p`_h * q`_(k - h) * (p`_j * q`_(k - j)) = \sum_(1 <= h < k) \sum_(h <= j < k) p`_h * q`_(k - h) * (p`_j * q`_(k - j)) + \sum_(1 <= i < k.+1) p`_i * q`_(k - i) * (p`_k * q`_0). rewrite (big_cat_nat (GRing.add_comoid R) (n:= k)) // big_nat1 big_nat1 [x in (_ = _ + x)](big_cat_nat (GRing.add_comoid R) (n:= k)) // big_nat1 (addnK k 0%N) Monoid.addmA. congr (_ + _). rewrite -big_split big_nat [x in (_ = x)]big_nat. apply: eq_bigr => i Hi. rewrite (big_cat_nat (GRing.add_comoid R) (n:= k)) //. by rewrite big_nat1 (addnK k 0%N). apply: ltnW. by case/andP : Hi. rewrite H {H} !opprD -!sumrN !addrA -[x in (x + _)]addrA -big_split -[x in ((((x + _) + _) + _) + _)]addrA [x in (((((_ + x) + _) + _) + _) + _)]addrC !addrA -big_split -addrA [x in (_ + x)]addrC !addrA addrC !addrA -big_split. have H : \big[GRing.add_comoid R/0]_(1 <= i < k) (GRing.add_comoid R) ((GRing.add_comoid R) (- (\sum_(i <= j < k) p`_i * q`_(k.+1 - i) * (p`_j * q`_(k.-1 - j)))) (- (\sum_(i <= j < k) p`_i.-1 * q`_(k - i) * (p`_j.+1 * q`_(k - j))))) ((GRing.add_comoid R) (\big[GRing.add_comoid R/0]_(i <= j < k) (p`_j.+1 * q`_(k - j.+1) * (p`_i.-1 * q`_(k - i.-1)))) (\sum_(i <= j < k) p`_i * q`_(k - i) * (p`_j * q`_(k - j)))) = \sum_(1 <= h < k) \sum_(h <= j < k) (p`_h * p`_j - p`_h.-1 * p`_j.+1) * (q`_(k - h) * q`_(k - j) - q`_(k.+1 - h) * q`_(k.-1 - j)). rewrite big_nat [x in (_ = x)]big_nat. apply: eq_bigr => i Hi. case/andP: Hi => Hi1 Hi2. rewrite -!sumrN -!big_split big_nat [x in (_ = x)]big_nat. apply: eq_bigr => j Hj. case/andP: Hj => Hj1 Hj2. rewrite /= -/(nth 0 _ j.+1) !addrA addrC. by rewrite -mulrN -!mulrA !addrA -(mulrDr p`_i) -mulrN !mulrA (mulrC _ p`_j) (mulrC _ p`_j) -!mulrA -(mulrDr p`_j) mulrN mulrA -[x in ((_ * _) + x + _ = _)]mulNr [x in (_ + (_ * x) + _ = _)]mulrA [x in (_ + (_ * (x * _)) + _ = _)]mulrC !mulrA [x in (_ + ((x * _) * _) + _ = _)]mulNr -[x in (_ + _ + (x * _) = _)]mulrA [x in (_ + _ + (_ * x * _) = _)]mulrC !mulrA [x in (_ + _ + (x * _ * _) = _)]mulrC -{2}(opprK (p`_i.-1 * p`_j.+1)) -[x in (_ + _ + x = _)]mulrA (mulNr (-(p`_i.-1 * p`_j.+1))) -[x in (_ + _ + x = _)]mulrN -addrA -[x in (_ + (x + _) = _)]mulrA -(mulrDr (- (p`_i.-1 * p`_j.+1))) [x in (_ + _ * (_ - x) = _)]mulrC -{2}(subn1 i) subnBA // addn1 -{2}(addn1 j) (addnC j 1%N) subnDA subn1 -mulrDl. rewrite H {H} -!addrA. apply: addr_ge0. rewrite big_nat; apply: sumr_ge0 => i Hi. rewrite big_nat; apply: sumr_ge0 => j Hj. apply: mulr_ge0. rewrite subr_ge0 [x in (_ <= x)]mulrC. apply: (normal_coef_chain_2 Hpzero Hpnormal). by case/andP : Hi. by case/andP : Hj. rewrite subr_ge0 [x in (x <= _)]mulrC -subn1 -subnDA addnC addn1 subnS subSn; last by rewrite ltnW; case/andP : Hi. apply: (normal_coef_chain_2 Hqzero Hqnormal). rewrite subn_gt0. by case/andP : Hj. rewrite leq_sub //. by case/andP : Hj. rewrite addrA [x in (0 <= _ + x)]addrC -!addrA [x in (0 <= _ + x)]addrA -big_split addrC -!addrA addr_ge0 //. rewrite big_nat; apply: sumr_ge0 => i Hi. rewrite /= -/(nth 0 _ (k.+1)) -/(nth 0 _ 0) [x in (0 <= x * _ - _)]mulrC [x in (0 <= _ - x * _)]mulrC -!mulrA -mulrBr. apply: mulr_ge0. by have/normalP [H _ _ _] := Hqnormal. rewrite !mulrA -mulrBl. apply: mulr_ge0. rewrite subr_ge0 [x in (_ <= x)]mulrC (normal_coef_chain_2 Hpzero Hpnormal) //. by case/andP : Hi. rewrite -ltnS; by case/andP : Hi. by have/normalP [H _ _ _] := Hqnormal. rewrite big_nat_recr// addrA -big_split addr_ge0 //. rewrite big_nat; apply: sumr_ge0 => i Hi. rewrite /= -/(nth 0 _ (k.+1)) -/(nth 0 _ (i.+1)) -/(nth 0 _ 0) mulrC addrC -!mulrA -mulrBr mulr_ge0 //. by have/normalP [H _ _ _] := Hpnormal. rewrite mulrC mulrA [x in (0 <= x * _ - _)]mulrC -!mulrA -mulrBr mulr_ge0 //. by have/normalP [H _ _ _] := Hpnormal. rewrite subn0 subr_ge0 -subn1 -subnDA addnC subnDA subn1. apply: (normal_coef_chain_2 Hqzero Hqnormal). rewrite subn_gt0; by case/andP : Hi. by rewrite -{2}(subn0 k) leq_sub. rewrite subn0 (addnK k 0%N). have/normalP [Hp _ _ _] := Hpnormal. have/normalP [Hq _ _ _] := Hqnormal. by apply: mulr_ge0; apply: mulr_ge0; by rewrite ?Hp ?Hq. rewrite big_add1 -pred_Sn. apply: eq_bigr => j _. by rewrite -pred_Sn. rewrite prod_all_ge0 // ?normal_neq0 // ?normal_neq0// => [k Hk| k Hk| ]. rewrite normal_0notroot_2 //. rewrite -ltnS prednK // in Hk. by rewrite size_poly_gt0 normal_neq0. rewrite normal_0notroot_2 //. rewrite -ltnS prednK // in Hk. by rewrite size_poly_gt0 normal_neq0. by apply: ltnW. 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)