proposition: Lemma pad_correct pi pr : pi >:: pr -> pi >:: pad pi pr.
proof: Proof. move=> Hp k. rewrite /PolR.nth nth_take_dflt. case: ifP => Hk. rewrite Pol.nth_default //; exact: J.zero_correct. rewrite nth_set_nth /= ifF; first exact: Hp. by apply/negP => /eqP K; rewrite K leqnn in Hk. 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