proposition: Lemma RiemannInt_Chasles : forall (f:R -> R) (a b c:R) (pr1:Riemann_integrable f a b) (pr2:Riemann_integrable f b c) (pr3:Riemann_integrable f a c), RiemannInt pr1 + RiemannInt pr2 = RiemannInt pr3.
proof: Proof. apply RiemannInt_P26. Qed.
imports: PeanoNat Reals Lra RiemannInt Rfunction_classes_def Rextensionality