proposition: Lemma RInt_plus : forall f g a b, ex_RInt f a b -> ex_RInt g a b -> RInt (fun x => plus (f x) (g x)) a b = plus (RInt f a b) (RInt g a b).
proof: Proof. intros f g a b Hf Hg. apply is_RInt_unique. apply: is_RInt_plus ; now apply RInt_correct. Qed.
imports: Coq(Reals Psatz) mathcomp(ssreflect ssrbool ssrfun eqtype seq) Markov Rcomplements Rbar Lub Lim_seq SF_seq Continuity Hierarchy