proposition: Lemma NewtonInt_P4 : forall (f:R -> R) (a b:R) (pr:Newton_integrable f a b), NewtonInt f a b pr = - NewtonInt f b a (NewtonInt_P3 f a b pr).
proof: Proof. intros f a b (x,H). unfold NewtonInt, NewtonInt_P3; simpl; ring. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis