proposition: Lemma RiemannInt_P340 : forall (f:R -> R) (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: 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.
imports: Reals integrales RiemannInt