proposition: Lemma nonneg_mulr (p q : {poly R}) : nonneg p -> nonneg q -> nonneg (p * q).
proof: Proof. have [->|Hpsize] := eqVneq p 0; first by rewrite mul0r. have [->|Hqsize Hp Hq] := eqVneq q 0; first by rewrite mulr0. apply/nonnegP => k lpq. rewrite coef_mul_poly /= sumr_ge0 // => i _. apply: mulr_ge0. have [Hi2|Hi2] := ltnP i (size p); first exact/nonnegP. by rewrite -(coefK p) coef_poly ltnNge Hi2. have [Hi2|Hi2] := ltnP (k - i) (size q); first exact/nonnegP. by rewrite -(coefK q) coef_poly ltnNge Hi2. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly polydiv polyorder ssrnum zmodp) mathcomp(polyrcf qe_rcf_th complex) poly_normal pol