proposition: Lemma ler_horner_norm_pol {R : realFieldType} (l : {poly R}) x : (0 <= x)%R -> `|l.[x]| <= \sum_(i < size l) (`|l`_i| * x ^+ i).
proof: Proof. move=> xge0; elim/poly_ind: l => [ | l a Ih]. by rewrite !hornerE normr0 size_poly0 big_ord0. rewrite hornerE. have [->|ln0] := eqVneq l 0%R. rewrite mul0r !hornerE size_polyC. have [->|an0] := eqVneq a 0%R; first by rewrite normr0 big_ord0. by rewrite big_ord1 /= expr0 mulr1 coefC eqxx. rewrite size_MXaddC (negbTE ln0) /= big_ord_recl expr0 mulr1. rewrite (le_trans (ler_norm_add _ _))//. rewrite coefD coefMX eqxx add0r coefC eqxx hornerE [X in X <= _]addrC. rewrite ler_add// !hornerE. have exteq (i : 'I_(size l)) : true -> `|(l * 'X + a%:P)`_(lift ord0 i)| * x ^+ lift ord0 i = (`|l`_i| * x ^+ i) * x. move=> _; rewrite lift0 coefD coefC /= addr0 coefMX /=. by rewrite exprS (mulrC x) mulrA. rewrite normrM (ger0_norm xge0). by rewrite (eq_bigr _ exteq) -mulr_suml ler_wpmul2r. Qed.
imports: mathcomp(all_ssreflect all_algebra) pol desc