proposition: Lemma RInt_Derive (f : R -> R) (a b : R): (forall x, Rmin a b <= x <= Rmax a b -> ex_derive f x) -> (forall x, Rmin a b <= x <= Rmax a b -> continuous (Derive f) x) -> RInt (Derive f) a b = f b - f a.
proof: Proof. intros Df Cdf. apply is_RInt_unique. apply: is_RInt_derive => //. intros ; by apply Derive_correct, Df. 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