proposition: Lemma contains_RInt prec (f3 : R -> R) x1 x2 Y X1 X2 : ex_RInt f3 x1 x2-> contains (I.convert X1) (Xreal x1) -> contains (I.convert X2) (Xreal x2) -> (forall x, (Rmin x1 x2 <= x <= Rmax x1 x2)%R -> contains (I.convert Y) (Xreal (f3 x))) -> contains (I.convert (I.mul prec (I.sub prec X2 X1) Y)) (Xreal (RInt f3 x1 x2)).
proof: Proof. intros Hf3_int HZx1 HZx2 Hext. destruct (Req_dec x2 x1) as [H|H]. { rewrite H, RInt_point. unfold zero ; simpl. rewrite <- (Rmult_0_l (f3 x1)). apply mul_correct. rewrite <- (Rminus_diag_eq x2 x1) by easy. now apply sub_correct. apply Hext. apply Rmin_Rmax_l. } replace (RInt f3 x1 x2) with ((x2 - x1) * ((RInt f3 x1 x2) / (x2 - x1)))%R. 2: { field. now apply Rminus_eq_contra. } apply mul_correct. now apply sub_correct. assert (H': forall x1 x2 : R, x1 < x2 -> (forall x, Rmin x1 x2 <= x <= Rmax x1 x2 -> contains (I.convert Y) (Xreal (f3 x))) -> ex_RInt f3 x1 x2 -> contains (I.convert Y) (Xreal (RInt f3 x1 x2 / (x2 - x1)))). 2: { destruct (Rdichotomy _ _ H) as [H21|H12]. apply ex_RInt_swap in Hf3_int. rewrite <- opp_RInt_swap by easy. replace (-_/_)%R with (RInt f3 x2 x1 / (x1 - x2))%R by (field; lra). apply H' ; try easy. now rewrite Rmin_comm, Rmax_comm. now apply H'. } clear. intros x1 x2 H' Hext Hf3_int. destruct (I.convert Y) as [|l u]. easy. apply le_contains. - destruct l as [|rl]. easy. unfold le_lower, le_upper. simpl. apply Ropp_le_contravar. apply RInt_le_l ; try easy. intros x Hx. apply Hext. now rewrite -> Rmin_left, Rmax_right ; try apply Rlt_le. - destruct u as [|ru]. easy. unfold le_upper. apply RInt_le_r ; try easy. intros x Hx. apply Hext. now rewrite -> Rmin_left, Rmax_right ; try apply Rlt_le. Qed.
imports: Coq(Bool Reals Psatz) Coquelicot(Coquelicot) Stdlib Xreal Basic