fact: Axiom 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.
imports: Reals