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