proposition: Lemma is_derive_RInt' (f If : R -> V) (a b : R) : locally a (fun a => is_RInt f a b (If a)) -> continuous f a -> is_derive If a (opp (f a)).
proof: Proof. intros. apply is_derive_ext with (fun x => opp (opp (If x))). intros ; by rewrite opp_opp. apply is_derive_opp. apply is_derive_RInt with b => //. move: H ; apply filter_imp. intros x 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