proposition: Lemma ex_RInt_gen_Chasles : forall {Fa Fc : (R -> Prop) -> Prop}, forall {FFa : Filter Fa} {FFc : Filter Fc}, forall (f : R -> V) (b : R), ex_RInt_gen f Fa (at_point b) -> ex_RInt_gen f (at_point b) Fc -> ex_RInt_gen f Fa Fc.
proof: Proof. intros Fa Fc FFa FFc f b [Iab Hab] [Ibc Hbc]. exists (plus Iab Ibc). now apply is_RInt_gen_Chasles with b. Qed.
imports: Coq(Reals ssreflect) Rbar Hierarchy RInt Lim_seq Continuity Derive Rcomplements RInt_analysis