proposition: Lemma RiemannInt_P32 : forall (f:C1_fun) (a b:R), Riemann_integrable (derive f (diff0 f)) a b.
proof: Proof. intro f; intros; destruct (Rle_dec a b) as [Hle|Hnle]; [ apply continuity_implies_RiemannInt; try assumption; intros; apply (cont1 f) | assert (H : b <= a); [ auto with real | apply RiemannInt_P1; apply continuity_implies_RiemannInt; try assumption; intros; apply (cont1 f) ] ]. Qed.
imports: Rfunctions SeqSeries Ranalysis_reg Rbase RiemannInt_SF RList Lra