proposition: Lemma poly_accr_bound1P p a r x y : `|x - a| <= r -> `|y - a| <= r -> `|p.[y] - p.[x]| <= `|y - x| * poly_accr_bound p a r.
proof: Proof. have [|r_lt0] := lerP 0 r; last first. by move=> hr; have := le_lt_trans hr r_lt0; rewrite normr_lt0. rewrite le0r=> /orP[/eqP->|r_gt0 hx hy]. by rewrite !normr_le0 !subr_eq0=> /eqP-> /eqP->; rewrite !subrr normr0 mul0r. rewrite mulrA mulrDr mulr1 ler_paddl ?mulr_ge0 ?normr_ge0 //=. by rewrite exprn_ge0 ?le_maxr ?mulr_ge0 ?ger0E ?ltW. rewrite -{1}(addNKr x y) [- _ + _]addrC /= -mulrA. rewrite nderiv_taylor; last exact: mulrC. have [->|p_neq0] := eqVneq p 0. rewrite size_poly0 big_ord0 horner0 subr0 normr0 mulr_ge0 ?normr_ge0 //. by rewrite big_ord0 mulr0 lexx. rewrite -[size _]prednK ?lt0n ?size_poly_eq0 //. rewrite big_ord_recl expr0 mulr1 nderivn0 addrC addKr !mulr_sumr. have := le_trans (ler_norm_sum _ _ _); apply. rewrite ler_sum // => i _. rewrite exprSr mulrA !normrM mulrC ler_wpmul2l ?normr_ge0 //. suff /ler_wpmul2l /le_trans : `|(y - x) ^+ i| <= maxr 1 (2%:R * r) ^+ (size p).-1. apply; rewrite ?normr_ge0 // mulrC ler_wpmul2l ?poly_boundP //. by rewrite ?exprn_ge0 // le_maxr ler01 mulr_ge0 ?ler0n ?ltW. case: (leP _ 1)=> hr. rewrite expr1n normrX exprn_ile1 ?normr_ge0 //. rewrite (le_trans (ler_dist_add a _ _)) // addrC distrC. by rewrite (le_trans _ hr) // mulrDl ler_add ?mul1r. apply: le_trans (_ : (2%:R * r) ^+ i <= _). rewrite normrX ler_expn2r -?topredE /= ?normr_ge0 ?mulr_ge0 ?ler0n //. by rewrite ltW. rewrite (le_trans (ler_dist_add a _ _)) // addrC distrC. by rewrite mulrDl ler_add ?mul1r. by rewrite ler_eexpn2l // ltnW. 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)