proposition: Lemma RiemannInt_P330 : forall (f:R -> R)(H : derivable f) (cont1 : continuity (derive f H)) (a b:R) (pr:Riemann_integrable (derive f H) a b), a <= b -> RiemannInt pr = f b - f a.
proof: Proof. intro f; intros; assert (H1 : forall x:R, a <= x <= b -> continuity_pt (derive f H) x). intros; apply (cont1). rewrite (RiemannInt_P20 H0 (FTC_P1 H0 H1) pr); assert (H2 := RiemannInt_P29 H0 H1); assert (H3 := RiemannInt_P310 f H cont1 a b H0); elim (antiderivative_Ucte (derive f H) _ _ _ _ H2 H3); intros C H4; repeat rewrite H4; [ ring | split; [ right; reflexivity | assumption ] | split; [ assumption | right; reflexivity ] ]. Qed.
imports: Reals integrales RiemannInt