proposition: Lemma all_pos_positive (p : {poly R}) x: all_ge0 p -> 0 <= x -> p.[x] >= 0.
proof: Proof. move=> h x0; rewrite horner_coef. apply: sumr_ge0 => [] [i his _] /=. apply: mulr_ge0; rewrite ?exprn_ge0 //; apply: (allP h); exact: mem_nth. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype order) mathcomp(binomial bigop ssralg poly ssrnum ssrint rat) mathcomp(polyrcf) pol