proposition: Lemma NewtonInt_P9 : forall (f:R -> R) (a b c:R) (pr1:Newton_integrable f a b) (pr2:Newton_integrable f b c), NewtonInt f a c (NewtonInt_P8 f a b c pr1 pr2) = NewtonInt f a b pr1 + NewtonInt f b c pr2.
proof: Proof. intros; unfold NewtonInt. case (NewtonInt_P8 f a b c pr1 pr2) as (x,Hor). case pr1 as (x0,Hor0). case pr2 as (x1,Hor1). destruct (total_order_T a b) as [[Hlt|Heq]|Hgt]. - destruct (total_order_T b c) as [[Hlt'|Heq']|Hgt']. + case Hor0; intro. 2:{ unfold antiderivative in H; elim H; clear H; intros _ H. elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H Hlt)). } case Hor1; intro. 2:{ unfold antiderivative in H0; elim H0; clear H0; intros _ H0. elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H0 Hlt')). } case Hor; intro. 2:{ unfold antiderivative in H1; elim H1; clear H1; intros _ H1. elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H1 (Rlt_trans _ _ _ Hlt Hlt'))). } assert (H2 := antiderivative_P2 f x0 x1 a b c H H0). assert (H3 := antiderivative_Ucte f x (fun x:R => match Rle_dec x b with | left _ => x0 x | right _ => x1 x + (x0 b - x1 b) end) a c H1 H2). elim H3; intros. assert (H5 : a <= a <= c). { split; [ right; reflexivity | left; apply Rlt_trans with b; assumption ]. } assert (H6 : a <= c <= c). { split; [ left; apply Rlt_trans with b; assumption | right; reflexivity ]. } rewrite (H4 _ H5); rewrite (H4 _ H6). destruct (Rle_dec a b) as [Hlea|Hnlea]. { destruct (Rle_dec c b) as [Hlec|Hnlec]. { elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ Hlec Hlt')). } ring. } elim Hnlea; left; assumption. + rewrite <- Heq'. unfold Rminus; rewrite Rplus_opp_r; rewrite Rplus_0_r. rewrite <- Heq' in Hor. elim Hor0; intro. 2:{ unfold antiderivative in H; elim H; clear H; intros _ H. elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H Hlt)). } elim Hor; intro. 2:{ unfold antiderivative in H0; elim H0; clear H0; intros _ H0. elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H0 Hlt)). } assert (H1 := antiderivative_Ucte f x x0 a b H0 H). elim H1; intros. rewrite (H2 b). { rewrite (H2 a). { ring. } split; [ right; reflexivity | left; assumption ]. } split; [ left; assumption | right; reflexivity ]. + elim Hor1; intro. { unfold antiderivative in H; elim H; clear H; intros _ H. elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H Hgt')). } elim Hor0; intro. 2:{ unfold antiderivative in H0; elim H0; clear H0; intros _ H0. elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H0 Hlt)). } elim Hor; intro. * assert (H2 := antiderivative_P2 f x x1 a c b H1 H). assert (H3 := antiderivative_Ucte _ _ _ a b H0 H2). elim H3; intros. rewrite (H4 a). { rewrite (H4 b). { destruct (Rle_dec b c) as [Hle|Hnle]. { elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ Hle Hgt')). } destruct (Rle_dec a c) as [Hle'|Hnle']. { ring. } elim Hnle'; unfold antiderivative in H1; elim H1; intros; assumption. } split; [ left; assumption | right; reflexivity ]. } split; [ right; reflexivity | left; assumption ]. * assert (H2 := antiderivative_P2 _ _ _ _ _ _ H1 H0). assert (H3 := antiderivative_Ucte _ _ _ c b H H2). elim H3; intros. rewrite (H4 c). { rewrite (H4 b). { destruct (Rle_dec b a) as [Hle|Hnle]. { elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ Hle Hlt)). } destruct (Rle_dec c a) as [Hle'|[]]. { ring. } unfold antiderivative in H1; elim H1; intros; assumption. } split; [ left; assumption | right; reflexivity ]. } split; [ right; reflexivity | left; assumption ]. - rewrite Heq in Hor |- *. elim Hor; intro. + elim Hor1; intro. * assert (H1 := antiderivative_Ucte _ _ _ b c H H0). elim H1; intros. assert (H3 : b <= c). { unfold antiderivative in H; elim H; intros; assumption. } rewrite (H2 b). { rewrite (H2 c). { ring. } split; [ assumption | right; reflexivity ]. } split; [ right; reflexivity | assumption ]. * assert (H1 : b = c). { unfold antiderivative in H, H0; elim H; elim H0; intros; apply Rle_antisym; assumption. } rewrite H1; ring. + elim Hor1; intro. * assert (H1 : b = c). { unfold antiderivative in H, H0; elim H; elim H0; intros; apply Rle_antisym; assumption. } rewrite H1; ring. * assert (H1 := antiderivative_Ucte _ _ _ c b H H0). elim H1; intros. assert (H3 : c <= b). { unfold antiderivative in H; elim H; intros; assumption. } rewrite (H2 c). { rewrite (H2 b). { ring. } split; [ assumption | right; reflexivity ]. } split; [ right; reflexivity | assumption ]. - destruct (total_order_T b c) as [[Hlt'|Heq']|Hgt']. + elim Hor0; intro. { unfold antiderivative in H; elim H; clear H; intros _ H. elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H Hgt)). } elim Hor1; intro. 2:{ unfold antiderivative in H0; elim H0; clear H0; intros _ H0. elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H0 Hlt')). } elim Hor; intro. * assert (H2 := antiderivative_P2 _ _ _ _ _ _ H H1). assert (H3 := antiderivative_Ucte _ _ _ b c H0 H2). elim H3; intros. rewrite (H4 b). { rewrite (H4 c). { case (Rle_dec b a) as [|[]]. { case (Rle_dec c a) as [|]. { assert (H5 : a = c). { unfold antiderivative in H1; elim H1; intros; apply Rle_antisym; assumption. } rewrite H5; ring. } ring. } left; assumption. } split; [ left; assumption | right; reflexivity ]. } split; [ right; reflexivity | left; assumption ]. * assert (H2 := antiderivative_P2 _ _ _ _ _ _ H0 H1). assert (H3 := antiderivative_Ucte _ _ _ b a H H2). elim H3; intros. rewrite (H4 a). 2:{ split; [ left; assumption | right; reflexivity ]. } rewrite (H4 b). 2:{ split; [ right; reflexivity | left; assumption ]. } case (Rle_dec b c) as [|[]]. 2:{ left; assumption. } case (Rle_dec a c) as [|]. { assert (H5 : a = c). { unfold antiderivative in H1; elim H1; intros; apply Rle_antisym; assumption. } rewrite H5; ring. } ring. + rewrite <- Heq'. unfold Rminus; rewrite Rplus_opp_r; rewrite Rplus_0_r. rewrite <- Heq' in Hor. elim Hor0; intro. { unfold antiderivative in H; elim H; clear H; intros _ H. elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H Hgt)). } elim Hor; intro. { unfold antiderivative in H0; elim H0; clear H0; intros _ H0. elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H0 Hgt)). } assert (H1 := antiderivative_Ucte f x x0 b a H0 H). elim H1; intros. rewrite (H2 b). { rewrite (H2 a). { ring. } split; [ left; assumption | right; reflexivity ]. } split; [ right; reflexivity | left; assumption ]. + elim Hor0; intro. { unfold antiderivative in H; elim H; clear H; intros _ H. elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H Hgt)). } elim Hor1; intro. { unfold antiderivative in H0; elim H0; clear H0; intros _ H0. elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H0 Hgt')). } elim Hor; intro. { unfold antiderivative in H1; elim H1; clear H1; intros _ H1. elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H1 (Rlt_trans _ _ _ Hgt' Hgt))). } assert (H2 := antiderivative_P2 _ _ _ _ _ _ H0 H). assert (H3 := antiderivative_Ucte _ _ _ c a H1 H2). elim H3; intros. assert (H5 : c <= a). { unfold antiderivative in H1; elim H1; intros; assumption. } rewrite (H4 c). { rewrite (H4 a). { destruct (Rle_dec a b) as [Hle|Hnle]. { elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ Hle Hgt)). } destruct (Rle_dec c b) as [|[]]. { ring. } left; assumption. } split; [ assumption | right; reflexivity ]. } split; [ right; reflexivity | assumption ]. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis