proposition: Lemma size_pad pi pr : eq_size pi (pad pi pr).
proof: Proof. rewrite /PolR.size size_take size_set_nth ifT //. exact: leq_maxl. 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