proposition: Lemma FTCN_step1 : forall (f:Differential) (a b:R), Newton_integrable (fun x:R => derive_pt f x (cond_diff f x)) a b.
proof: Proof. intros f a b; unfold Newton_integrable; exists (d1 f); unfold antiderivative; intros; case (Rle_dec a b); intro; [ left; split; [ intros; exists (cond_diff f x); reflexivity | assumption ] | right; split; [ intros; exists (cond_diff f x); reflexivity | auto with real ] ]. Defined.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis