proposition: Lemma continuous_RInt_1 (f : R -> V) (a b : R) (If : R -> V) : locally b (fun z : R => is_RInt f a z (If z)) -> continuous If b.
proof: Proof. intros. generalize (locally_singleton _ _ H) => /= Hab. apply continuous_ext with (fun z => plus (If b) (minus (If z) (If b))) ; simpl. intros x. by rewrite plus_comm -plus_assoc plus_opp_l plus_zero_r. eapply filterlim_comp_2, filterlim_plus. apply filterlim_const. apply (continuous_RInt_0 f _ (fun x : R_UniformSpace => minus (If x) (If b))). apply: filter_imp H => x Hx. rewrite /minus plus_comm. eapply is_RInt_Chasles, Hx. by apply is_RInt_swap. 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