proposition: Lemma RiemannInt_bound_exchange_1 : forall (f : R -> R) (a b : R) (pr1 : Riemann_integrable f a b), RiemannInt pr1 = - RiemannInt (Riemann_integrable_opp_bound f a b pr1).
proof: Proof. intros. rewrite (RiemannInt_bound_exchange f a b pr1 (Riemann_integrable_opp_bound f a b pr1)). reflexivity. Qed.
imports: PeanoNat Reals Lra RiemannInt Rfunction_classes_def Rextensionality