proposition: Lemma RiemannInt_plus : forall (f g : R -> R) (a b : R) (pr_f : Riemann_integrable f a b) (pr_g : Riemann_integrable g a b) (pr : Riemann_integrable (fun x => f x + g x) a b), RiemannInt pr = RiemannInt pr_f + RiemannInt pr_g.
proof: Proof. intros. rewrite <- (Rmult_1_l (RiemannInt pr_g)). rewrite <- (RiemannInt_P13 pr_f pr_g (RiemannInt_P10 1 pr_f pr_g)). apply RiemannInt_ext. intros ; ring. Qed.
imports: Coq(Reals Psatz ssreflect) Coq(ssrbool) mathcomp(seq)