proposition: Lemma Rint_derive : forall f a b d, a <= b -> (forall x, a <= x <= b -> derivable_pt_abs f x (d x)) -> (forall x, a <= x <= b -> continuity_pt d x) -> Rint d a b (f b - f a).
proof: Proof. intros f a b d Hab Hder Hcont. pose proof prolongement_C1_C1 f d a b Hab Hder Hcont as [g [Heq Hdeq]]. apply Rint_eq_compat with (derive g (diff0 g)). rewrite Rmin_def, Rmax_def; assumption. exists (RiemannInt_P32 g a b). rewrite RiemannInt_P33; intuition. do 2 (rewrite Heq; intuition). Qed.
imports: Reals RiemannInt RIneq Lra R_sqr MyRfunctions