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 ; intro ; apply RiemannInt_derivable_pt ; apply Hconta. Qed.
imports: Reals Rintegral Riemann_integrable Rfunction_classes Nth_derivative_def Lra Ring Ranalysis Rextensionality