proposition: Lemma Rint_derive2 : forall f a b d, (forall x, Rmin a b <= x <= Rmax a b -> derivable_pt_abs f x (d x)) -> (forall x, Rmin a b <= x <= Rmax a b -> continuity_pt d x) -> Rint d a b (f b - f a).
proof: Proof. intros f a b d Hder Hcont. destruct (Rle_dec a b) as [n|n]. rewrite Rmin_def, Rmax_def in *; try assumption. apply Rint_derive; assumption. apply Rnot_le_lt, Rlt_le in n. rewrite Rmin_comm, Rmax_comm, Rmin_def, Rmax_def in *; try assumption. apply Rint_reverse_1; replace (- (f b - f a)) with (f a - f b) by ring. apply Rint_derive; assumption. Qed.
imports: Reals RiemannInt RIneq Lra R_sqr MyRfunctions