proposition: Lemma NewtonInt_P2 : forall (f:R -> R) (a:R), NewtonInt f a a (NewtonInt_P1 f a) = 0.
proof: Proof. intros; unfold NewtonInt; simpl; unfold mult_fct, fct_cte, id. destruct NewtonInt_P1 as [g _]. now apply Rminus_diag_eq. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis