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