proposition: Lemma is_RInt_gen_plus {Fa Fb : (R -> Prop) -> Prop} {FFa : Filter Fa} {FFb : Filter Fb} (f g : R -> V) (lf lg : V) : is_RInt_gen f Fa Fb lf -> is_RInt_gen g Fa Fb lg -> is_RInt_gen (fun y => plus (f y) (g y)) Fa Fb (plus lf lg).
proof: Proof. intros Hf Hg P HP. move /filterlim_plus in HP. destruct HP as [Q R HQ HR H]. specialize (Hf _ HQ). specialize (Hg _ HR). unfold filtermapi in Hf, Hg |- *. apply: filter_imp (filter_and _ _ Hf Hg). move => [a b] /= [[If [HIf1 HIf2]] [Ig [HIg1 HIg2]]]. exists (plus If Ig). apply: conj (H _ _ HIf2 HIg2). exact: is_RInt_plus. Qed.
imports: Coq(Reals ssreflect) Rbar Hierarchy RInt Lim_seq Continuity Derive Rcomplements RInt_analysis