proposition: Lemma size_TM_power_int (p : Z) (X0 X : I.type) (n : nat) : Pol.size (approx (TM_power_int p X0 X n)) = n.+1.
proof: Proof. rewrite /TM_power_int. case: p => [|p|p]; last case: apart0; by rewrite (@Pol.size_dotmuldiv (n.+1)) ?(Pol.size_rec1, size_rec1up). 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