proposition: Lemma RiemannInt_minus_1 : forall (f g:R -> R) (a b:R) (prf:Riemann_integrable f a b) (prg:Riemann_integrable g a b), a<=b -> RiemannInt prf - RiemannInt prg = RiemannInt (RiemannInt_integrable_minus f g a b prf prg).
proof: Proof. intros. rewrite (RiemannInt_minus _ _ _ _ prf prg) ; intuition. Qed.
imports: PeanoNat Reals Lra RiemannInt Rfunction_classes_def Rextensionality