proposition: Lemma Derive_RInt (f : R -> R) (a b : R) : locally b (ex_RInt f a) -> continuous f b -> Derive (RInt f a) b = f b.
proof: Proof. intros If Cf. apply is_derive_unique, (is_derive_RInt _ _ a) => //. 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