proposition: Lemma all_pos_increasing (p : {poly R}): all_ge0 p -> {in <=%R 0 &, pol_increasing p}.
proof: Proof. move=> posp x y le0x le0y lexy; rewrite !horner_coef. apply: ler_sum => [] [i ihs] /= _. apply: ler_wpmul2l => //; first by apply: (allP posp); exact: mem_nth. by apply: ler_expn2r. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype order) mathcomp(binomial bigop ssralg poly ssrnum ssrint rat) mathcomp(polyrcf) pol