proposition: Lemma RiemannInt_P30 : forall (f:R -> R) (a b:R), a <= b -> (forall x:R, a <= x <= b -> continuity_pt f x) -> { g:R -> R | antiderivative f g a b }.
proof: Proof. intros; split with (primitive H (FTC_P1 H H0)); apply RiemannInt_P29. Qed.
imports: Rfunctions SeqSeries Ranalysis_reg Rbase RiemannInt_SF RList Lra