proposition: Lemma RiemannInt_P31 : forall (f:C1_fun) (a b:R), a <= b -> antiderivative (derive f (diff0 f)) f a b.
proof: Proof. intro f; intros; unfold antiderivative; split; try assumption; intros; split with (diff0 f x); reflexivity. Qed.
imports: Rfunctions SeqSeries Ranalysis_reg Rbase RiemannInt_SF RList Lra