proposition: Lemma RiemannInt_continuity : forall a t0 (Hconta : continuity a) (Ha : forall t0 t, Riemann_integrable a t0 t), continuity (fun t => RiemannInt (Ha t0 t)).
proof: Proof. intros. apply derivable_continuous. unfold derivable. intros. apply RiemannInt_derivable_pt. apply Hconta. Qed.
imports: PeanoNat Reals Lra RiemannInt Rfunction_classes_def Rextensionality