proposition: Lemma poly_accr_bound2P p (a r x y : F) : (x != y)%B -> `|x - a| <= r -> `|y - a| <= r -> `|(p.[y] - p.[x]) / (y - x) - p^`().[x]| <= `|y - x| * poly_accr_bound2 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]. rewrite !normr_le0 !subr_eq0. by move=> nxy /eqP xa /eqP xb; rewrite xa xb eqxx in nxy. move=> neq_xy hx hy. 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. by rewrite derivC !horner0 size_poly0 !(big_ord0, subrr, mul0r) normr0 !mulr0. rewrite -[size _]prednK ?lt0n ?size_poly_eq0 //. rewrite big_ord_recl expr0 mulr1 nderivn0 /= -size_deriv. have [->|p'_neq0] := eqVneq p^`() 0. by rewrite horner0 size_poly0 !big_ord0 addr0 !(subrr, mul0r) normr0 !mulr0. rewrite -[size _]prednK ?lt0n ?size_poly_eq0 // big_ord_recl expr1. rewrite addrAC subrr add0r mulrDl mulfK; last by rewrite subr_eq0 eq_sym. rewrite nderivn1 addrAC subrr add0r mulr_sumr normrM normfV. rewrite ler_pdivr_mulr ?normr_gt0; last by rewrite subr_eq0 eq_sym. rewrite mulrAC -expr2 mulrC mulr_suml. have := le_trans (ler_norm_sum _ _ _); apply. rewrite ler_sum // => i _ /=; rewrite /bump /= !add1n. rewrite normrM normrX 3!exprSr expr1 !mulrA !ler_wpmul2r ?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 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 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)