proposition: Lemma Riemann_integrable_continuity : forall (f:R -> R) (a b:R), a < b -> (forall x:R, a <= x <= b -> continuity_pt f x) -> Riemann_integrable f a b.
proof: Proof. apply RiemannInt_P6. Qed.
imports: PeanoNat Reals Lra RiemannInt Rfunction_classes_def Rextensionality