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