proposition: Lemma RiemannInt_integrable_minus : forall (f g:R -> R) (a b:R) (prf:Riemann_integrable f a b) (prg:Riemann_integrable g a b), (Riemann_integrable (fun x => f x - g x) a b).
proof: Proof. intros. apply RiemannInt_integrable_eq_compat with (fun x => f x + (-1) * g x); [intros; ring|]. apply RiemannInt_P10; assumption. Qed.
imports: PeanoNat Reals Lra RiemannInt Rfunction_classes_def Rextensionality