proposition: Lemma derivable_primitive : forall (f:R -> R) (a b x:R) (h:a <= b) (C0:forall x:R, a <= x <= b -> continuity_pt f x), a <= x <= b -> derivable_pt_lim (primitive h (FTC_P1 h C0)) x (f x).
proof: Proof. apply RiemannInt_P28. Qed.
imports: PeanoNat Reals Lra RiemannInt Rfunction_classes_def Rextensionality