proposition: Lemma RInt_Chasles_bound_comp_l_loc (f : R -> R -> R) (a : R -> R) (b x : R) : locally x (fun y => ex_RInt (f y) (a x) b) -> (exists eps : posreal, locally x (fun y => ex_RInt (f y) (a x - eps) (a x + eps))) -> continuous a x -> locally x (fun x' => RInt (f x') (a x') (a x) + RInt (f x') (a x) b = RInt (f x') (a x') b).
proof: Proof. intros Hab (eps,Hae) Ca. generalize (proj1 (filterlim_locally _ _) Ca) => {} Ca. generalize (filter_and _ _ (Ca eps) (filter_and _ _ Hab Hae)). apply filter_imp => {Ca Hae Hab} y [Hy [Hab Hae]]. apply RInt_Chasles with (2 := Hab). apply ex_RInt_inside with (1 := Hae). now apply Rlt_le. rewrite /Rminus Rplus_opp_r Rabs_R0. apply Rlt_le, cond_pos. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(eqtype seq) Markov Rcomplements Rbar Lub Lim_seq Derive SF_seq Continuity Hierarchy Seq_fct RInt PSeries