proposition: Lemma NewtonInt_P6 : forall (f g:R -> R) (l a b:R) (pr1:Newton_integrable f a b) (pr2:Newton_integrable g a b), NewtonInt (fun x:R => l * f x + g x) a b (NewtonInt_P5 f g l a b pr1 pr2) = l * NewtonInt f a b pr1 + NewtonInt g a b pr2.
proof: Proof. intros f g l a b pr1 pr2; unfold NewtonInt; destruct (NewtonInt_P5 f g l a b pr1 pr2) as (x,o); destruct pr1 as (x0,o0); destruct pr2 as (x1,o1); destruct (total_order_T a b) as [[Hlt|Heq]|Hgt]. - elim o; intro. 2:{ unfold antiderivative in H; elim H; intros; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H1 Hlt)). } elim o0; intro. 2:{ unfold antiderivative in H0; elim H0; intros; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H2 Hlt)). } elim o1; intro. 2:{ unfold antiderivative in H1; elim H1; intros; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H3 Hlt)). } assert (H2 := antiderivative_P1 f g x0 x1 l a b H0 H1); assert (H3 := antiderivative_Ucte _ _ _ _ _ H H2); elim H3; intros; assert (H5 : a <= a <= b). { split; [ right; reflexivity | left; assumption ]. } assert (H6 : a <= b <= b). { split; [ left; assumption | right; reflexivity ]. } assert (H7 := H4 _ H5); assert (H8 := H4 _ H6); rewrite H7; rewrite H8; ring. - rewrite Heq; ring. - elim o; intro. { unfold antiderivative in H; elim H; intros; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H1 Hgt)). } elim o0; intro. { unfold antiderivative in H0; elim H0; intros; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H2 Hgt)). } elim o1; intro. { unfold antiderivative in H1; elim H1; intros; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H3 Hgt)). } assert (H2 := antiderivative_P1 f g x0 x1 l b a H0 H1); assert (H3 := antiderivative_Ucte _ _ _ _ _ H H2); elim H3; intros; assert (H5 : b <= a <= a). { split; [ left; assumption | right; reflexivity ]. } assert (H6 : b <= b <= a). { split; [ right; reflexivity | left; assumption ]. } assert (H7 := H4 _ H5); assert (H8 := H4 _ H6); rewrite H7; rewrite H8; ring. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis