proposition: Lemma ex_RInt_Chasles_0 (f : R -> V) (a b c : R) : a <= b <= c -> ex_RInt f a b -> ex_RInt f b c -> ex_RInt f a c.
proof: Proof. case => Hab Hbc H1 H2. case: Hab => [ Hab | -> ] //. case: Hbc => [ Hbc | <- ] //. case: H1 => [l1 H1] ; case: H2 => [l2 H2]. exists (plus l1 l2). apply is_RInt_Chasles_0 with b ; try assumption. by split. Qed.
imports: Coq(Reals Psatz) mathcomp(ssreflect ssrbool ssrfun eqtype seq) Markov Rcomplements Rbar Lub Lim_seq SF_seq Continuity Hierarchy