proposition: Lemma Riemann_integrable_plus : forall (f g : R -> R) (a b : R), Riemann_integrable f a b -> Riemann_integrable g a b -> Riemann_integrable (fun x => f x + g x) a b.
proof: Proof. intros f g a b pr_f pr_g. apply (Riemann_integrable_ext (fun x => f x + 1 * g x)). intros ; ring. apply (RiemannInt_P10 1 pr_f pr_g). Qed.
imports: Coq(Reals Psatz ssreflect) Coq(ssrbool) mathcomp(seq)