proposition: Lemma is_RInt_gen_Chasles {Fa Fc : (R -> Prop) -> Prop} {FFa : Filter Fa} {FFc : Filter Fc} (f : R -> V) (b : R) (l1 l2 : V) : is_RInt_gen f Fa (at_point b) l1 -> is_RInt_gen f (at_point b) Fc l2 -> is_RInt_gen f Fa Fc (plus l1 l2).
proof: Proof. intros Hab Hbc P HP. specialize (filterlim_plus _ _ P HP). intros [Q R HQ HR H]. specialize (Hab Q HQ). specialize (Hbc R HR). destruct Hab as [Qa Ra HQa HRa Hab]. destruct Hbc as [Qc Rc HQc HRc Hbc]. apply: Filter_prod HQa HRc _. intros a c Ha Hc. specialize (Hab _ _ Ha HRa). specialize (Hbc _ _ HQc Hc). destruct Hab as [ya [Hya1 Hya2]]. destruct Hbc as [yc [Hyc1 Hyc2]]. exists (plus ya yc). split. apply: is_RInt_Chasles Hya1 Hyc1. now apply H. Qed.
imports: Coq(Reals ssreflect) Rbar Hierarchy RInt Lim_seq Continuity Derive Rcomplements RInt_analysis