proposition: Lemma taylor_integral_correct : contains (I.convert taylor_integral) (Xreal (RInt f a b)).
proof: Proof. rewrite /taylor_integral. apply: (@TM.TMI.integralEnclosure_correct prec X0 X (fun x => Xreal (f x)) Mf (proj_val (I.F.convert (I.midpoint X)))) => //. apply J.contains_midpoint. now exists a. Qed.
imports: Coq(Reals List Psatz) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool) Stdlib Coquelicot Xreal Interval Taylor_model Interval_compl