proposition: Lemma RiemannInt_derivable_pt : forall (f:R -> R) (a x:R) (pr:forall x y:R, Riemann_integrable f x y) (Hcont:continuity_pt f x), derivable_pt (fun t1 => @RiemannInt f a t1 (pr a t1)) x.
proof: Proof. intros. unfold derivable_pt, derivable_pt_abs. exists (f x). apply RiemannInt_derivable_pt_lim. assumption. Qed.
imports: PeanoNat Reals Lra RiemannInt Rfunction_classes_def Rextensionality