proposition: Lemma contains_interval_float_integral (p : PolR.T) : approx Mf >:: p -> TM_integral_poly >:: (PolR.primitive tt 0%R p).
proof: Proof. move=> Hp; rewrite /TM_integral_poly. by apply: Pol.primitive_correct; first exact: J.zero_correct. 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