proposition: Lemma taylor_integral_naive_intersection_correct : contains (I.convert taylor_integral_naive_intersection) (Xreal (RInt f a b)).
proof: Proof. rewrite /taylor_integral_naive_intersection. set tmp := I.mul prec (I.sub prec ib ia) (iF (I.join ia ib)). generalize (I.real_correct tmp). case I.real ; intros Hr. 2: now destruct (I.convert tmp). apply I.meet_correct. apply J.contains_RInt => //. intros x Hx. apply HiFIntExt. assert (H := I.join_correct ia ib). apply: contains_connected Hx. apply H. now apply Rmin_case ; [left|right]. apply H. now apply Rmax_case ; [left|right]. exact: taylor_integral_correct. Qed.
imports: Coq(Reals List Psatz) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool) Stdlib Coquelicot Xreal Interval Taylor_model Interval_compl