proposition: Lemma size_TM_var (X X0 : I.type) : Pol.size (approx (TM_var X X0)) = 2.
proof: Proof. rewrite /TM_var Pol.size_set_nth Pol.polyXE Pol.size_lift Pol.oneE Pol.polyCE. by rewrite Pol.size_polyCons Pol.size_polyNil. 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