proposition: Lemma Riemann_integrable_add : forall (f g:R -> R) (a b:R) (pr1:Riemann_integrable f a b) (pr2:Riemann_integrable g a b), Riemann_integrable (f + g)%F a b.
proof: Proof. intros. apply RiemannInt_integrable_eq_compat with (fun x => f x + 1 * g x). intros. unfold plus_fct. ring. apply Riemann_integrable_linear ; assumption. Qed.
imports: PeanoNat Reals Lra RiemannInt Rfunction_classes_def Rextensionality