proposition: Lemma Riemann_integrable_continuity_gen : 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 continuity_implies_RiemannInt. Qed.
imports: PeanoNat Reals Lra RiemannInt Rfunction_classes_def Rextensionality