proposition: Lemma RiemannInt_P33 : forall (f:C1_fun) (a b:R) (pr:Riemann_integrable (derive f (diff0 f)) a b), a <= b -> RiemannInt pr = f b - f a.
proof: Proof. intro f; intros; assert (H0 : forall x:R, a <= x <= b -> continuity_pt (derive f (diff0 f)) x). { intros; apply (cont1 f). } rewrite (RiemannInt_P20 H (FTC_P1 H H0) pr); assert (H1 := RiemannInt_P29 H H0); assert (H2 := RiemannInt_P31 f H); elim (antiderivative_Ucte (derive f (diff0 f)) _ _ _ _ H1 H2); intros C H3; repeat rewrite H3; [ ring | split; [ right; reflexivity | assumption ] | split; [ assumption | right; reflexivity ] ]. Qed.
imports: Rfunctions SeqSeries Ranalysis_reg Rbase RiemannInt_SF RList Lra