proposition: Lemma Derive_RInt' (f : R -> R) (a b : R) : locally a (fun a => ex_RInt f a b) -> continuous f a -> Derive (fun a => RInt f a b) a = - f a.
proof: Proof. intros If Cf. eapply is_derive_unique, (is_derive_RInt' (V := R_NormedModule) _ _ a b) => //. move: If ; apply filter_imp => y. exact: RInt_correct. 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