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