proposition: Lemma integralEnclosure_correct : i_validTM x0 iX Mf xF -> contains (I.convert integralEnclosure) (Xreal (RInt f a b)).
proof: Proof. move => [Hdef Hnai Hcontains0 HX0X H]. have {H} [q HMfq Herror] := H. have HI: ex_RInt (fun x => q.[x - x0]) a b by exact: pol_int_sub. have ->: RInt f a b = RInt (fun x => q.[x - x0]) a b + RInt (fun x => f x - q.[x - x0]) a b. rewrite RInt_minus //. by rewrite -[minus _ _]/(Rplus _ (Ropp _)) Rplus_comm Rplus_assoc Rplus_opp_l Rplus_0_r. apply: J.add_correct. rewrite RInt_translation_sub. rewrite Rpol_integral_0. have H: forall x xi, xi >: x -> Pol.horner prec TM_integral_poly (Isub xi X0) >: (PolR.primitive tt 0 q).[x - x0]. move => x xi Hx. apply: Pol.horner_correct. exact: Pol.primitive_correct J.zero_correct HMfq. exact: J.sub_correct. apply: J.sub_correct ; exact: H. eapply ex_RInt_ext. 2: apply: ex_RInt_translation_add HI. intros t. by rewrite /= /Rminus Rplus_assoc Rplus_opp_r Rplus_0_r. apply: J.contains_RInt => //. exact: ex_RInt_minus. move => x Hx. apply: Herror. apply: contains_connected Hx. now apply Rmin_case. now apply Rmax_case. 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