proposition: Lemma NewtonInt_P3 : forall (f:R -> R) (a b:R) (X:Newton_integrable f a b), Newton_integrable f b a.
proof: Proof. unfold Newton_integrable; intros; elim X; intros g H; exists g; tauto. Defined.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis