proposition: Lemma ex_RInt_Chasles (f : R -> V) (a b c : R) : ex_RInt f a b -> ex_RInt f b c -> ex_RInt f a c.
proof: Proof. intros [l1 H1] [l2 H2]. exists (plus l1 l2). by apply is_RInt_Chasles with b. Qed.
imports: Coq(Reals Psatz) mathcomp(ssreflect ssrbool ssrfun eqtype seq) Markov Rcomplements Rbar Lub Lim_seq SF_seq Continuity Hierarchy