proposition: Lemma derive_pt_RiemannInt_1 : forall (f:R -> R) (a x:R) (pr:forall x y:R, Riemann_integrable f x y) (Hcont:continuity_pt f x) H1, derive_pt (fun t => RiemannInt (pr a t)) x H1 = f x.
proof: Proof. intros. rewrite derive_pt_eq. apply RiemannInt_derivable_pt_lim. apply Hcont. Qed.
imports: PeanoNat Reals Lra RiemannInt Rfunction_classes_def Rextensionality