proposition: Lemma RiemannInt_minus : forall (f g:R -> R) (a b:R) (prf:Riemann_integrable f a b) (prg:Riemann_integrable g a b) (prfg:Riemann_integrable (fun x:R => f x - g x) a b), a<=b -> RiemannInt prfg = RiemannInt prf - RiemannInt prg.
proof: Proof. intros. assert (REW: forall x y, x - y = x + (-1)*y) by (intros; ring); rewrite REW; clear REW. pose proof (RiemannInt_P10 (-1) prf prg) as prfg'. replace (RiemannInt prfg) with (RiemannInt prfg'). apply RiemannInt_P13. apply RiemannInt_P18 ; intuition. ring. Qed.
imports: PeanoNat Reals Lra RiemannInt Rfunction_classes_def Rextensionality