proposition: Lemma NewtonInt_P1 : forall (f:R -> R) (a:R), Newton_integrable f a a.
proof: Proof. intros f a; unfold Newton_integrable; exists (fct_cte (f a) * id)%F; left; unfold antiderivative; split. 2:right;reflexivity. intros; assert (H1 : derivable_pt (fct_cte (f a) * id) x). { apply derivable_pt_mult. { apply derivable_pt_const. } apply derivable_pt_id. } exists H1; assert (H2 : x = a). { elim H; intros; apply Rle_antisym; assumption. } symmetry ; apply derive_pt_eq_0; replace (f x) with (0 * id x + fct_cte (f a) x * 1); [ apply (derivable_pt_lim_mult (fct_cte (f a)) id x); [ apply derivable_pt_lim_const | apply derivable_pt_lim_id ] | unfold id, fct_cte; rewrite H2; ring ]. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis