fact: Definition taylor_integral_naive_intersection := let temp := I.mul prec (I.sub prec ib ia) (iF (I.join ia ib)) in if I.real temp then I.meet temp taylor_integral else temp.
imports: Coq(Reals List Psatz) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool) Stdlib Coquelicot Xreal Interval Taylor_model Interval_compl