proposition: Lemma nonnegP (s : seq R) : reflect (forall k, (k < size s)%N -> 0 <= s`_k) (nonneg s).
proof: Proof. exact/all_nthP. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly polydiv polyorder ssrnum zmodp) mathcomp(polyrcf qe_rcf_th complex) poly_normal pol