proposition: Lemma nonneg_root_nonpos (p : {poly R}) : p \is monic -> (forall z : C, root (toC p) z -> (Re z <= 0)) -> nonneg p.
proof: Proof. move=> Hpmonic. move: {2}(size p) (leqnn (size p)) => n. elim: n p Hpmonic=> [p Hpmonic Hpsize Hproot | n IH p Hpmonic Hpsize Hproots]. rewrite size_poly_leq0 in Hpsize. by rewrite (eqP Hpsize) monicE lead_coef0 eq_sym oner_eq0 in Hpmonic. case: (altP (size (toC p) =P 1%N)) => Hpsize2. rewrite size_map_poly_id0 in Hpsize2; last by rewrite eq_sym negbT // lt_eqF // ltcR (eqP Hpmonic) ltr01. have Hp := (size1_polyC (eq_leq Hpsize2)). rewrite Hp in Hpsize2. rewrite Hp monicE lead_coefE Hpsize2 -pred_Sn polyseqC in Hpmonic. rewrite size_polyC in Hpsize2. rewrite Hpsize2 /= in Hpmonic. by rewrite Hp /= (eqP Hpmonic) polyseqC oner_neq0 /= ler01. move/closed_rootP : Hpsize2. case=> x Hrootx. have [Himx|Himx] := altP (Im x =P 0). have H := monicXsubC (Re x). have Hp := real_root_div_poly_deg1 Himx Hrootx. rewrite Pdiv.IdomainMonic.dvdp_eq // in Hp. rewrite (eqP Hp) nonneg_mulr //. apply: IH=> [ | | z Hz]. + by rewrite monicE -(@lead_coef_Mmonic _ (p %/ ('X - (Re x)%:P)) ('X - (Re x)%:P)) // -(eqP Hp) -monicE. - rewrite size_divp; last by apply: monic_neq0. by rewrite size_XsubC leq_subLR addnC addn1. + rewrite Hproots // (eqP Hp) rmorphM rootM. apply/orP; by left. by rewrite nonneg_poly_deg1 (Hproots x Hrootx). have H : 'X^2 + (1 *- 2 * Re x) *: 'X + (Re x ^+ 2 + Im x ^+ 2)%:P \is monic. by rewrite -(mul1r 'X^2) mul_polyC monicE lead_coefE polyseq_deg2 // oner_neq0. have H2 : size ('X^2 + (1 *- 2 * Re x) *: 'X + (Re x ^+ 2 + Im x ^+ 2)%:P) = 3%N. by rewrite -(mul1r 'X^2) mul_polyC polyseq_deg2 // oner_neq0. have Hp := complex_root_div_poly_deg2 Himx Hrootx. rewrite Pdiv.IdomainMonic.dvdp_eq // in Hp. rewrite (eqP Hp) nonneg_mulr //. apply: IH=> [ | | z Hz]. + by rewrite monicE -(@lead_coef_Mmonic _ _ ('X^2 + (1 *- 2 * Re x) *: 'X + (Re x ^+ 2 + Im x ^+ 2)%:P)) // -(eqP Hp) -monicE. - rewrite size_divp; last by apply: monic_neq0. by rewrite H2 leq_subLR addnC addn2 (@leq_trans n.+1). + by rewrite Hproots // (eqP Hp) rmorphM rootM Hz. by rewrite nonneg_poly_deg2 (Hproots _ Hrootx). Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly polydiv polyorder ssrnum zmodp) mathcomp(polyrcf qe_rcf_th complex) poly_normal pol