proposition: Lemma NewtonInt_P8 : forall (f:R -> R) (a b c:R), Newton_integrable f a b -> Newton_integrable f b c -> Newton_integrable f a c.
proof: Proof. intros. elim X; intros F0 H0. elim X0; intros F1 H1. destruct (total_order_T a b) as [[Hlt|Heq]|Hgt]. - destruct (total_order_T b c) as [[Hlt'|Heq']|Hgt']. + unfold Newton_integrable; exists (fun x:R => match Rle_dec x b with | left _ => F0 x | right _ => F1 x + (F0 b - F1 b) end). elim H0; intro. { elim H1; intro. { left; apply antiderivative_P2; assumption. } unfold antiderivative in H2; elim H2; clear H2; intros _ H2. elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H2 Hlt')). } unfold antiderivative in H; elim H; clear H; intros _ H. elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H Hlt)). + rewrite Heq' in X; apply X. + destruct (total_order_T a c) as [[Hlt''|Heq'']|Hgt'']. * unfold Newton_integrable; exists F0. left. elim H1; intro. { unfold antiderivative in H; elim H; clear H; intros _ H. elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H Hgt')). } elim H0; intro. { assert (H3 := antiderivative_P3 f F0 F1 a b c H2 H). elim H3; intro. { unfold antiderivative in H4; elim H4; clear H4; intros _ H4. elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H4 Hlt'')). } assumption. } unfold antiderivative in H2; elim H2; clear H2; intros _ H2. elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H2 Hlt)). * rewrite Heq''; apply NewtonInt_P1. * unfold Newton_integrable; exists F1. right. elim H1; intro. { unfold antiderivative in H; elim H; clear H; intros _ H. elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H Hgt')). } elim H0; intro. { assert (H3 := antiderivative_P3 f F0 F1 a b c H2 H). elim H3; intro. { assumption. } unfold antiderivative in H4; elim H4; clear H4; intros _ H4. elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H4 Hgt'')). } unfold antiderivative in H2; elim H2; clear H2; intros _ H2. elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H2 Hlt)). - rewrite Heq; apply X0. - destruct (total_order_T b c) as [[Hlt'|Heq']|Hgt']. + destruct (total_order_T a c) as [[Hlt''|Heq'']|Hgt'']. * unfold Newton_integrable; exists F1. left. elim H1; intro. { elim H0; intro. { unfold antiderivative in H2; elim H2; clear H2; intros _ H2. elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H2 Hgt)). } assert (H3 := antiderivative_P4 f F0 F1 b a c H2 H). elim H3; intro. { assumption. } unfold antiderivative in H4; elim H4; clear H4; intros _ H4. elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H4 Hlt'')). } unfold antiderivative in H; elim H; clear H; intros _ H. elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H Hlt')). * rewrite Heq''; apply NewtonInt_P1. * unfold Newton_integrable; exists F0. right. elim H0; intro. { unfold antiderivative in H; elim H; clear H; intros _ H. elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H Hgt)). } elim H1; intro. { assert (H3 := antiderivative_P4 f F0 F1 b a c H H2). elim H3; intro. { unfold antiderivative in H4; elim H4; clear H4; intros _ H4. elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H4 Hgt'')). } assumption. } unfold antiderivative in H2; elim H2; clear H2; intros _ H2. elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H2 Hlt')). + rewrite Heq' in X; apply X. + assert (X1 := NewtonInt_P3 f a b X). assert (X2 := NewtonInt_P3 f b c X0). apply NewtonInt_P3. apply NewtonInt_P7 with b; assumption. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis