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