proposition: Lemma FTC_Newton : forall (f:Differential) (a b:R), NewtonInt (fun x:R => derive_pt f x (cond_diff f x)) a b (FTCN_step1 f a b) = f b - f a.
proof: Proof. intros; unfold NewtonInt; reflexivity. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis