proposition: Lemma RInt_gen_Chasles : forall {V : CompleteNormedModule R_AbsRing} {Fa Fc : (R -> Prop) -> Prop}, forall {FFa : ProperFilter' Fa} {FFc : ProperFilter' Fc}, forall (f : R -> V) (b : R), ex_RInt_gen f Fa (at_point b) -> ex_RInt_gen f (at_point b) Fc -> plus (RInt_gen f Fa (at_point b)) (RInt_gen f (at_point b) Fc) = RInt_gen f Fa Fc.
proof: Proof. intros V Fa Fc FFa FFc f b Hab Hbc. apply esym, is_RInt_gen_unique. apply: is_RInt_gen_Chasles. now apply RInt_gen_correct. now apply RInt_gen_correct. Qed.
imports: Coq(Reals Psatz) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Stdlib MathComp