proposition: Lemma horner_pad pi pr x : pi >:: pr -> pr.[x] = (pad pi pr).[x].
proof: Proof. move=> Hp. rewrite !(@PolR.hornerE_wide (maxn (Pol.size pi) (PolR.size pr))) -?size_pad; rewrite ?(leq_maxl, leq_maxr) //. apply: eq_bigr => i _. congr Rmult. rewrite /pad /PolR.nth nth_take_dflt /PolR.nth nth_set_nth. case: ifP => [Hi| /negbT Hi]. by rewrite [LHS](Pol.nth_default_alt Hp). rewrite -ltnNge in Hi; rewrite /= ifF //. by apply/negbTE; rewrite neq_ltn Hi. Qed.
imports: Coq(ZArith Psatz Reals) Flocq(Raux) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Stdlib MathComp Coquelicot Xreal Interval Basic Xreal_derive Interval_compl Datatypes Taylor_poly Basic_rec Bound