proposition: Lemma RiemannInt_add : forall (f g:R -> R) (a b:R) (prf:Riemann_integrable f a b) (prg:Riemann_integrable g a b) (prfg:Riemann_integrable (f + g)%F a b), a <= b -> RiemannInt prf + RiemannInt prg = RiemannInt prfg.
proof: Proof. intros. pose proof (RiemannInt_P10 1 prf prg) as prfg'. replace (RiemannInt prfg) with (RiemannInt prfg'). replace (RiemannInt prg) with (1 * RiemannInt prg) by ring. symmetry. apply RiemannInt_P13. apply RiemannInt_P18 ; intuition. unfold plus_fct. ring. Qed.
imports: PeanoNat Reals Lra RiemannInt Rfunction_classes_def Rextensionality