proposition: Lemma NewtonInt_P7 : forall (f:R -> R) (a b c:R), a < b -> b < c -> Newton_integrable f a b -> Newton_integrable f b c -> Newton_integrable f a c.
proof: Proof. unfold Newton_integrable; intros f a b c Hab Hbc X X0; elim X; clear X; intros F0 H0; elim X0; clear X0; intros F1 H1; set (g := fun x:R => match Rle_dec x b with | left _ => F0 x | right _ => F1 x + (F0 b - F1 b) end); exists g; left; unfold g; apply antiderivative_P2. { elim H0; intro. { assumption. } unfold antiderivative in H; elim H; clear H; intros; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H2 Hab)). } elim H1; intro. { assumption. } unfold antiderivative in H; elim H; clear H; intros; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H2 Hbc)). Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis