# Library Coqtail.Reals.Ediff.realisation_by_stdlib

Require Import Reals.
Require Import integrales.
Require Import RiemannInt.

Lemma continuity_implies_RiemannInt1 : (f:RR) (a b:R),
( x:R, (a x b b x a) → continuity_pt f x) → Riemann_integrable f a b.
Proof.
intros.
destruct (Rle_dec a b).
apply continuity_implies_RiemannInt; intuition.
assert (b a) ; intuition.
apply RiemannInt_P1.
apply continuity_implies_RiemannInt; intuition.
Qed.

Lemma RiemannInt_P320 : (f:RR) (H : derivable f) (cont1 : continuity (derive f H))(a b:R), Riemann_integrable (derive f H) a b.
Proof.
intro f; intros; case (Rle_dec a b); intro;
[ apply continuity_implies_RiemannInt; try assumption; intros;
apply (cont1)
| assert (H1 : b a);
[ auto with real
| apply RiemannInt_P1; apply continuity_implies_RiemannInt;
try assumption; intros; apply (cont1) ] ].
Qed.

Lemma RiemannInt_P310 : (f:RR) (H : derivable f) (cont1 : continuity (derive f H)) (a b:R),
a bantiderivative (derive f H) f a b.
Proof.
intro f; intros; unfold antiderivative in |- *; split; try assumption; intros;
split with (H x); reflexivity.
Qed.

Lemma RiemannInt_P330 : (f:RR)(H : derivable f) (cont1 : continuity (derive f H)) (a b:R) (pr:Riemann_integrable (derive f H) a b),
a bRiemannInt pr = f b - f a.
Proof.
intro f; intros;
assert
(H1 : x:R, a x bcontinuity_pt (derive f H) x).
intros; apply (cont1).
rewrite (RiemannInt_P20 H0 (FTC_P1 H0 H1) pr);
assert (H2 := RiemannInt_P29 H0 H1); assert (H3 := RiemannInt_P310 f H cont1 a b H0);
elim (antiderivative_Ucte (derive f H) _ _ _ _ H2 H3);
intros C H4; repeat rewrite H4;
[ ring
| split; [ right; reflexivity | assumption ]
| split; [ assumption | right; reflexivity ] ].
Qed.

Lemma RiemannInt_P340 : (f:RR) (H: derivable f) (cont1 : continuity (derive f H)) (a b:R) (pr:Riemann_integrable (derive f H) a b),
RiemannInt pr = f b - f a.
Proof.
intro f; intros; case (Rle_dec a b); intro.
apply RiemannInt_P330; assumption.
assert (H0 : b a);
[ auto with real
| assert (H1 := RiemannInt_P1 pr); rewrite (RiemannInt_P8 pr H1);
rewrite (RiemannInt_P330 _ _ cont1 b a H1 H0); ring ].
Qed.

Module Real_std_lib : Integrals.

Definition Riemann_integrable := Riemann_integrable.
Definition RiemannInt_P1 := RiemannInt_P1.
Definition RiemannInt := RiemannInt.
Definition RiemannInt_ext := RiemannInt_P5.
Definition Riemann_integrable_singleton := RiemannInt_P7.
Definition continuity_implies_RiemannInt := continuity_implies_RiemannInt1.
Definition RiemannInt_opp := RiemannInt_P8.
Definition RiemannInt_singleton := RiemannInt_P9.
Definition Riemann_integrable_linear := RiemannInt_P10.
Definition RiemannInt_linear := RiemannInt_P13.
Definition Riemann_integrable_const := RiemannInt_P14.
Definition RiemannInt_const := RiemannInt_P15.
Definition Riemann_integrable_Rabs := RiemannInt_P16.
Definition Riemann_integrable_chasles := RiemannInt_P24.
Definition RiemannInt_monotony := RiemannInt_P22.
Definition RiemannInt_monotony2 := RiemannInt_P23.
Definition RiemannInt_chasles := RiemannInt_P26.
Definition derive_Riemann_integrable := RiemannInt_P320.
Definition FTC_Riemann := RiemannInt_P340.

End Real_std_lib.