proposition: Lemma poly_boundP p a r x : `|x - a| <= r -> `|p.[x]| <= poly_bound p a r.
proof: Proof. have [r_ge0|r_lt0] := lerP 0 r; last first. by move=> hr; have := le_lt_trans hr r_lt0; rewrite normr_lt0. rewrite ler_distl=> /andP[lx ux]. rewrite ler_paddl //. elim/poly_ind: p=> [|p c ihp]. by rewrite horner0 normr0 size_poly0 big_ord0. rewrite hornerMXaddC size_MXaddC. have [->|p_neq0 /=] := altP eqP. rewrite horner0 !mul0r !add0r size_poly0. have [->|c_neq0] /= := altP eqP; first by rewrite normr0 big_ord0. rewrite big_ord_recl big_ord0 addr0 coefC /=. by rewrite ler_pmulr ?normr_gt0 // ler_addl ler_maxr !normr_ge0. rewrite big_ord_recl coefD coefMX coefC eqxx add0r. rewrite (le_trans (ler_norm_add _ _)) // addrC ler_add //. by rewrite expr0 mulr1. rewrite normrM. move: ihp=> /(ler_wpmul2r (normr_ge0 x)) /le_trans-> //. rewrite mulr_suml ler_sum // => i _. rewrite coefD coefC coefMX /= addr0 exprSr mulrA. rewrite ler_wpmul2l //. by rewrite ?mulr_ge0 ?exprn_ge0 ?ler_maxr ?addr_ge0 ?normr_ge0 // ltrW. rewrite (ger0_norm r_ge0) ler_norml opprD. rewrite (le_trans _ lx) ?(le_trans ux) // ler_add2r. by rewrite ler_normr lexx. by rewrite ler_oppl ler_normr lexx orbT. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop order ssralg ssrnum ssrint rat poly polydiv polyorder) mathcomp(perm matrix mxpoly polyXY binomial bigenough)