diff options
Diffstat (limited to 'theories/Reals/RiemannInt_SF.v')
| -rw-r--r-- | theories/Reals/RiemannInt_SF.v | 958 |
1 files changed, 478 insertions, 480 deletions
diff --git a/theories/Reals/RiemannInt_SF.v b/theories/Reals/RiemannInt_SF.v index d0d9519c..d523a1f4 100644 --- a/theories/Reals/RiemannInt_SF.v +++ b/theories/Reals/RiemannInt_SF.v @@ -1,18 +1,16 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: RiemannInt_SF.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Require Import Rbase. Require Import Rfunctions. -Require Import Ranalysis. +Require Import Ranalysis_reg. Require Import Classical_Prop. -Open Local Scope R_scope. +Local Open Scope R_scope. Set Implicit Arguments. @@ -23,7 +21,7 @@ Set Implicit Arguments. Definition Nbound (I:nat -> Prop) : Prop := exists n : nat, (forall i:nat, I i -> (i <= n)%nat). -Lemma IZN_var : forall z:Z, (0 <= z)%Z -> {n : nat | z = Z_of_nat n}. +Lemma IZN_var : forall z:Z, (0 <= z)%Z -> {n : nat | z = Z.of_nat n}. Proof. intros; apply Z_of_nat_complete_inf; assumption. Qed. @@ -35,19 +33,19 @@ Lemma Nzorn : Proof. intros I H H0; set (E := fun x:R => exists i : nat, I i /\ INR i = x); assert (H1 : bound E). - unfold Nbound in H0; elim H0; intros N H1; unfold bound in |- *; - exists (INR N); unfold is_upper_bound in |- *; intros; + unfold Nbound in H0; elim H0; intros N H1; unfold bound; + exists (INR N); unfold is_upper_bound; intros; unfold E in H2; elim H2; intros; elim H3; intros; rewrite <- H5; apply le_INR; apply H1; assumption. assert (H2 : exists x : R, E x). - elim H; intros; exists (INR x); unfold E in |- *; exists x; split; + elim H; intros; exists (INR x); unfold E; exists x; split; [ assumption | reflexivity ]. assert (H3 := completeness E H1 H2); elim H3; intros; unfold is_lub in p; elim p; clear p; intros; unfold is_upper_bound in H4, H5; assert (H6 : 0 <= x). elim H2; intros; unfold E in H6; elim H6; intros; elim H7; intros; apply Rle_trans with x0; - [ rewrite <- H9; change (INR 0 <= INR x1) in |- *; apply le_INR; + [ rewrite <- H9; change (INR 0 <= INR x1); apply le_INR; apply le_O_n | apply H4; assumption ]. assert (H7 := archimed x); elim H7; clear H7; intros; @@ -90,7 +88,7 @@ Proof. [ idtac | reflexivity ]; rewrite <- minus_INR. replace (x0 - 1)%nat with (pred x0); [ reflexivity - | case x0; [ reflexivity | intro; simpl in |- *; apply minus_n_O ] ]. + | case x0; [ reflexivity | intro; simpl; apply minus_n_O ] ]. induction x0 as [| x0 Hrecx0]; [ rewrite p in H7; rewrite <- INR_IZR_INZ in H7; simpl in H7; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H6 H7)) @@ -101,10 +99,10 @@ Proof. assert (H16 : INR x0 = INR x1 + 1). rewrite H15; ring. rewrite <- S_INR in H16; assert (H17 := INR_eq _ _ H16); rewrite H17; - simpl in |- *; split. + simpl; split. assumption. intros; apply INR_le; rewrite H15; rewrite <- H15; elim H12; intros; - rewrite H20; apply H4; unfold E in |- *; exists i; + rewrite H20; apply H4; unfold E; exists i; split; [ assumption | reflexivity ]. Qed. @@ -149,7 +147,7 @@ Definition subdivision_val (a b:R) (f:StepFun a b) : Rlist := | existT a b => a end. -Boxed Fixpoint Int_SF (l k:Rlist) : R := +Fixpoint Int_SF (l k:Rlist) : R := match l with | nil => 0 | cons a l' => @@ -175,7 +173,7 @@ Lemma StepFun_P1 : forall (a b:R) (f:StepFun a b), adapted_couple f a b (subdivision f) (subdivision_val f). Proof. - intros a b f; unfold subdivision_val in |- *; case (projT2 (pre f)); intros; + intros a b f; unfold subdivision_val; case (projT2 (pre f)); intros; apply a0. Qed. @@ -183,13 +181,13 @@ Lemma StepFun_P2 : forall (a b:R) (f:R -> R) (l lf:Rlist), adapted_couple f a b l lf -> adapted_couple f b a l lf. Proof. - unfold adapted_couple in |- *; intros; decompose [and] H; clear H; + unfold adapted_couple; intros; decompose [and] H; clear H; repeat split; try assumption. - rewrite H2; unfold Rmin in |- *; case (Rle_dec a b); intro; + rewrite H2; unfold Rmin; case (Rle_dec a b); intro; case (Rle_dec b a); intro; try reflexivity. apply Rle_antisym; assumption. apply Rle_antisym; auto with real. - rewrite H1; unfold Rmax in |- *; case (Rle_dec a b); intro; + rewrite H1; unfold Rmax; case (Rle_dec a b); intro; case (Rle_dec b a); intro; try reflexivity. apply Rle_antisym; assumption. apply Rle_antisym; auto with real. @@ -200,23 +198,23 @@ Lemma StepFun_P3 : a <= b -> adapted_couple (fct_cte c) a b (cons a (cons b nil)) (cons c nil). Proof. - intros; unfold adapted_couple in |- *; repeat split. - unfold ordered_Rlist in |- *; intros; simpl in H0; inversion H0; - [ simpl in |- *; assumption | elim (le_Sn_O _ H2) ]. - simpl in |- *; unfold Rmin in |- *; case (Rle_dec a b); intro; + intros; unfold adapted_couple; repeat split. + unfold ordered_Rlist; intros; simpl in H0; inversion H0; + [ simpl; assumption | elim (le_Sn_O _ H2) ]. + simpl; unfold Rmin; case (Rle_dec a b); intro; [ reflexivity | elim n; assumption ]. - simpl in |- *; unfold Rmax in |- *; case (Rle_dec a b); intro; + simpl; unfold Rmax; case (Rle_dec a b); intro; [ reflexivity | elim n; assumption ]. - unfold constant_D_eq, open_interval in |- *; intros; simpl in H0; + unfold constant_D_eq, open_interval; intros; simpl in H0; inversion H0; [ reflexivity | elim (le_Sn_O _ H3) ]. Qed. Lemma StepFun_P4 : forall a b c:R, IsStepFun (fct_cte c) a b. Proof. - intros; unfold IsStepFun in |- *; case (Rle_dec a b); intro. - apply existT with (cons a (cons b nil)); unfold is_subdivision in |- *; + intros; unfold IsStepFun; case (Rle_dec a b); intro. + apply existT with (cons a (cons b nil)); unfold is_subdivision; apply existT with (cons c nil); apply (StepFun_P3 c r). - apply existT with (cons b (cons a nil)); unfold is_subdivision in |- *; + apply existT with (cons b (cons a nil)); unfold is_subdivision; apply existT with (cons c nil); apply StepFun_P2; apply StepFun_P3; auto with real. Qed. @@ -234,7 +232,7 @@ Qed. Lemma StepFun_P6 : forall (f:R -> R) (a b:R), IsStepFun f a b -> IsStepFun f b a. Proof. - unfold IsStepFun in |- *; intros; elim X; intros; apply existT with x; + unfold IsStepFun; intros; elim X; intros; apply existT with x; apply StepFun_P5; assumption. Qed. @@ -244,26 +242,26 @@ Lemma StepFun_P7 : adapted_couple f a b (cons r1 (cons r2 l)) (cons r3 lf) -> adapted_couple f r2 b (cons r2 l) lf. Proof. - unfold adapted_couple in |- *; intros; decompose [and] H0; clear H0; + unfold adapted_couple; intros; decompose [and] H0; clear H0; assert (H5 : Rmax a b = b). - unfold Rmax in |- *; case (Rle_dec a b); intro; + unfold Rmax; case (Rle_dec a b); intro; [ reflexivity | elim n; assumption ]. assert (H7 : r2 <= b). rewrite H5 in H2; rewrite <- H2; apply RList_P7; - [ assumption | simpl in |- *; right; left; reflexivity ]. + [ assumption | simpl; right; left; reflexivity ]. repeat split. apply RList_P4 with r1; assumption. - rewrite H5 in H2; unfold Rmin in |- *; case (Rle_dec r2 b); intro; + rewrite H5 in H2; unfold Rmin; case (Rle_dec r2 b); intro; [ reflexivity | elim n; assumption ]. - unfold Rmax in |- *; case (Rle_dec r2 b); intro; + unfold Rmax; case (Rle_dec r2 b); intro; [ rewrite H5 in H2; rewrite <- H2; reflexivity | elim n; assumption ]. - simpl in H4; simpl in |- *; apply INR_eq; apply Rplus_eq_reg_l with 1; + simpl in H4; simpl; apply INR_eq; apply Rplus_eq_reg_l with 1; do 2 rewrite (Rplus_comm 1); do 2 rewrite <- S_INR; rewrite H4; reflexivity. - intros; unfold constant_D_eq, open_interval in |- *; intros; + intros; unfold constant_D_eq, open_interval; intros; unfold constant_D_eq, open_interval in H6; assert (H9 : (S i < pred (Rlength (cons r1 (cons r2 l))))%nat). - simpl in |- *; simpl in H0; apply lt_n_S; assumption. + simpl; simpl in H0; apply lt_n_S; assumption. assert (H10 := H6 _ H9); apply H10; assumption. Qed. @@ -280,19 +278,19 @@ Proof. discriminate. intros; induction lf1 as [| r3 lf1 Hreclf1]. reflexivity. - simpl in |- *; cut (r = r1). + simpl; cut (r = r1). intro; rewrite H3; rewrite (H0 lf1 r b). ring. rewrite H3; apply StepFun_P7 with a r r3; [ right; assumption | assumption ]. clear H H0 Hreclf1 r0; unfold adapted_couple in H1; decompose [and] H1; - intros; simpl in H4; rewrite H4; unfold Rmin in |- *; + intros; simpl in H4; rewrite H4; unfold Rmin; case (Rle_dec a b); intro; [ assumption | reflexivity ]. unfold adapted_couple in H1; decompose [and] H1; intros; apply Rle_antisym. - apply (H3 0%nat); simpl in |- *; apply lt_O_Sn. + apply (H3 0%nat); simpl; apply lt_O_Sn. simpl in H5; rewrite H2 in H5; rewrite H5; replace (Rmin b b) with (Rmax a b); [ rewrite <- H4; apply RList_P7; - [ assumption | simpl in |- *; right; left; reflexivity ] - | unfold Rmin, Rmax in |- *; case (Rle_dec b b); case (Rle_dec a b); intros; + [ assumption | simpl; right; left; reflexivity ] + | unfold Rmin, Rmax; case (Rle_dec b b); case (Rle_dec a b); intros; try assumption || reflexivity ]. Qed. @@ -305,10 +303,10 @@ Proof. [ simpl in H4; discriminate | induction l as [| r0 l Hrecl0]; [ simpl in H3; simpl in H2; generalize H3; generalize H2; - unfold Rmin, Rmax in |- *; case (Rle_dec a b); + unfold Rmin, Rmax; case (Rle_dec a b); intros; elim H0; rewrite <- H5; rewrite <- H7; reflexivity - | simpl in |- *; do 2 apply le_n_S; apply le_O_n ] ]. + | simpl; do 2 apply le_n_S; apply le_O_n ] ]. Qed. Lemma StepFun_P10 : @@ -322,12 +320,12 @@ Proof. intros; unfold adapted_couple in H0; decompose [and] H0; simpl in H4; discriminate. intros; case (Req_dec a b); intro. - exists (cons a nil); exists nil; unfold adapted_couple_opt in |- *; - unfold adapted_couple in |- *; unfold ordered_Rlist in |- *; + exists (cons a nil); exists nil; unfold adapted_couple_opt; + unfold adapted_couple; unfold ordered_Rlist; repeat split; try (intros; simpl in H3; elim (lt_n_O _ H3)). - simpl in |- *; rewrite <- H2; unfold Rmin in |- *; case (Rle_dec a a); intro; + simpl; rewrite <- H2; unfold Rmin; case (Rle_dec a a); intro; reflexivity. - simpl in |- *; rewrite <- H2; unfold Rmax in |- *; case (Rle_dec a a); intro; + simpl; rewrite <- H2; unfold Rmax; case (Rle_dec a a); intro; reflexivity. elim (RList_P20 _ (StepFun_P9 H1 H2)); intros t1 [t2 [t3 H3]]; induction lf as [| r1 lf Hreclf]. @@ -342,32 +340,32 @@ Proof. apply H6. rewrite <- Hyp_eq; rewrite H3 in H1; unfold adapted_couple in H1; decompose [and] H1; clear H1; simpl in H9; rewrite H9; - unfold Rmin in |- *; case (Rle_dec a b); intro; + unfold Rmin; case (Rle_dec a b); intro; [ reflexivity | elim n; assumption ]. elim H6; clear H6; intros l' [lf' H6]; case (Req_dec t2 b); intro. exists (cons a (cons b nil)); exists (cons r1 nil); - unfold adapted_couple_opt in |- *; unfold adapted_couple in |- *; + unfold adapted_couple_opt; unfold adapted_couple; repeat split. - unfold ordered_Rlist in |- *; intros; simpl in H8; inversion H8; - [ simpl in |- *; assumption | elim (le_Sn_O _ H10) ]. - simpl in |- *; unfold Rmin in |- *; case (Rle_dec a b); intro; + unfold ordered_Rlist; intros; simpl in H8; inversion H8; + [ simpl; assumption | elim (le_Sn_O _ H10) ]. + simpl; unfold Rmin; case (Rle_dec a b); intro; [ reflexivity | elim n; assumption ]. - simpl in |- *; unfold Rmax in |- *; case (Rle_dec a b); intro; + simpl; unfold Rmax; case (Rle_dec a b); intro; [ reflexivity | elim n; assumption ]. intros; simpl in H8; inversion H8. - unfold constant_D_eq, open_interval in |- *; intros; simpl in |- *; + unfold constant_D_eq, open_interval; intros; simpl; simpl in H9; rewrite H3 in H1; unfold adapted_couple in H1; decompose [and] H1; apply (H16 0%nat). - simpl in |- *; apply lt_O_Sn. - unfold open_interval in |- *; simpl in |- *; rewrite H7; simpl in H13; - rewrite H13; unfold Rmin in |- *; case (Rle_dec a b); + simpl; apply lt_O_Sn. + unfold open_interval; simpl; rewrite H7; simpl in H13; + rewrite H13; unfold Rmin; case (Rle_dec a b); intro; [ assumption | elim n; assumption ]. elim (le_Sn_O _ H10). intros; simpl in H8; elim (lt_n_O _ H8). intros; simpl in H8; inversion H8; - [ simpl in |- *; assumption | elim (le_Sn_O _ H10) ]. + [ simpl; assumption | elim (le_Sn_O _ H10) ]. assert (Hyp_min : Rmin t2 b = t2). - unfold Rmin in |- *; case (Rle_dec t2 b); intro; + unfold Rmin; case (Rle_dec t2 b); intro; [ reflexivity | elim n; assumption ]. unfold adapted_couple in H6; elim H6; clear H6; intros; elim (RList_P20 _ (StepFun_P9 H6 H7)); intros s1 [s2 [s3 H9]]; @@ -379,141 +377,141 @@ Proof. exists (cons t1 (cons s2 s3)); exists (cons r1 lf'); rewrite H3 in H1; rewrite H9 in H6; unfold adapted_couple in H6, H1; decompose [and] H1; decompose [and] H6; clear H1 H6; - unfold adapted_couple_opt in |- *; unfold adapted_couple in |- *; + unfold adapted_couple_opt; unfold adapted_couple; repeat split. - unfold ordered_Rlist in |- *; intros; simpl in H1; + unfold ordered_Rlist; intros; simpl in H1; induction i as [| i Hreci]. - simpl in |- *; apply Rle_trans with s1. + simpl; apply Rle_trans with s1. replace s1 with t2. apply (H12 0%nat). - simpl in |- *; apply lt_O_Sn. - simpl in H19; rewrite H19; symmetry in |- *; apply Hyp_min. - apply (H16 0%nat); simpl in |- *; apply lt_O_Sn. - change (pos_Rl (cons s2 s3) i <= pos_Rl (cons s2 s3) (S i)) in |- *; - apply (H16 (S i)); simpl in |- *; assumption. - simpl in |- *; simpl in H14; rewrite H14; reflexivity. - simpl in |- *; simpl in H18; rewrite H18; unfold Rmax in |- *; + simpl; apply lt_O_Sn. + simpl in H19; rewrite H19; symmetry ; apply Hyp_min. + apply (H16 0%nat); simpl; apply lt_O_Sn. + change (pos_Rl (cons s2 s3) i <= pos_Rl (cons s2 s3) (S i)); + apply (H16 (S i)); simpl; assumption. + simpl; simpl in H14; rewrite H14; reflexivity. + simpl; simpl in H18; rewrite H18; unfold Rmax; case (Rle_dec a b); case (Rle_dec t2 b); intros; reflexivity || elim n; assumption. - simpl in |- *; simpl in H20; apply H20. - intros; simpl in H1; unfold constant_D_eq, open_interval in |- *; intros; + simpl; simpl in H20; apply H20. + intros; simpl in H1; unfold constant_D_eq, open_interval; intros; induction i as [| i Hreci]. - simpl in |- *; simpl in H6; case (total_order_T x t2); intro. + simpl; simpl in H6; case (total_order_T x t2); intro. elim s; intro. apply (H17 0%nat); - [ simpl in |- *; apply lt_O_Sn - | unfold open_interval in |- *; simpl in |- *; elim H6; intros; split; + [ simpl; apply lt_O_Sn + | unfold open_interval; simpl; elim H6; intros; split; assumption ]. rewrite b0; assumption. rewrite H10; apply (H22 0%nat); - [ simpl in |- *; apply lt_O_Sn - | unfold open_interval in |- *; simpl in |- *; replace s1 with t2; + [ simpl; apply lt_O_Sn + | unfold open_interval; simpl; replace s1 with t2; [ elim H6; intros; split; assumption | simpl in H19; rewrite H19; rewrite Hyp_min; reflexivity ] ]. - simpl in |- *; simpl in H6; apply (H22 (S i)); - [ simpl in |- *; assumption - | unfold open_interval in |- *; simpl in |- *; apply H6 ]. + simpl; simpl in H6; apply (H22 (S i)); + [ simpl; assumption + | unfold open_interval; simpl; apply H6 ]. intros; simpl in H1; rewrite H10; change (pos_Rl (cons r2 lf') i <> pos_Rl (cons r2 lf') (S i) \/ f (pos_Rl (cons s1 (cons s2 s3)) (S i)) <> pos_Rl (cons r2 lf') i) - in |- *; rewrite <- H9; elim H8; intros; apply H6; - simpl in |- *; apply H1. + ; rewrite <- H9; elim H8; intros; apply H6; + simpl; apply H1. intros; induction i as [| i Hreci]. - simpl in |- *; red in |- *; intro; elim Hyp_eq; apply Rle_antisym. - apply (H12 0%nat); simpl in |- *; apply lt_O_Sn. + simpl; red; intro; elim Hyp_eq; apply Rle_antisym. + apply (H12 0%nat); simpl; apply lt_O_Sn. rewrite <- Hyp_min; rewrite H6; simpl in H19; rewrite <- H19; - apply (H16 0%nat); simpl in |- *; apply lt_O_Sn. - elim H8; intros; rewrite H9 in H21; apply (H21 (S i)); simpl in |- *; + apply (H16 0%nat); simpl; apply lt_O_Sn. + elim H8; intros; rewrite H9 in H21; apply (H21 (S i)); simpl; simpl in H1; apply H1. exists (cons t1 l'); exists (cons r1 (cons r2 lf')); rewrite H9 in H6; rewrite H3 in H1; unfold adapted_couple in H1, H6; decompose [and] H6; decompose [and] H1; clear H6 H1; - unfold adapted_couple_opt in |- *; unfold adapted_couple in |- *; + unfold adapted_couple_opt; unfold adapted_couple; repeat split. - rewrite H9; unfold ordered_Rlist in |- *; intros; simpl in H1; + rewrite H9; unfold ordered_Rlist; intros; simpl in H1; induction i as [| i Hreci]. - simpl in |- *; replace s1 with t2. - apply (H16 0%nat); simpl in |- *; apply lt_O_Sn. + simpl; replace s1 with t2. + apply (H16 0%nat); simpl; apply lt_O_Sn. simpl in H14; rewrite H14; rewrite Hyp_min; reflexivity. change (pos_Rl (cons s1 (cons s2 s3)) i <= pos_Rl (cons s1 (cons s2 s3)) (S i)) - in |- *; apply (H12 i); simpl in |- *; apply lt_S_n; + ; apply (H12 i); simpl; apply lt_S_n; assumption. - simpl in |- *; simpl in H19; apply H19. - rewrite H9; simpl in |- *; simpl in H13; rewrite H13; unfold Rmax in |- *; + simpl; simpl in H19; apply H19. + rewrite H9; simpl; simpl in H13; rewrite H13; unfold Rmax; case (Rle_dec t2 b); case (Rle_dec a b); intros; reflexivity || elim n; assumption. - rewrite H9; simpl in |- *; simpl in H15; rewrite H15; reflexivity. - intros; simpl in H1; unfold constant_D_eq, open_interval in |- *; intros; + rewrite H9; simpl; simpl in H15; rewrite H15; reflexivity. + intros; simpl in H1; unfold constant_D_eq, open_interval; intros; induction i as [| i Hreci]. - simpl in |- *; rewrite H9 in H6; simpl in H6; apply (H22 0%nat). - simpl in |- *; apply lt_O_Sn. - unfold open_interval in |- *; simpl in |- *. + simpl; rewrite H9 in H6; simpl in H6; apply (H22 0%nat). + simpl; apply lt_O_Sn. + unfold open_interval; simpl. replace t2 with s1. assumption. simpl in H14; rewrite H14; rewrite Hyp_min; reflexivity. - change (f x = pos_Rl (cons r2 lf') i) in |- *; clear Hreci; apply (H17 i). - simpl in |- *; rewrite H9 in H1; simpl in H1; apply lt_S_n; apply H1. - rewrite H9 in H6; unfold open_interval in |- *; apply H6. + change (f x = pos_Rl (cons r2 lf') i); clear Hreci; apply (H17 i). + simpl; rewrite H9 in H1; simpl in H1; apply lt_S_n; apply H1. + rewrite H9 in H6; unfold open_interval; apply H6. intros; simpl in H1; induction i as [| i Hreci]. - simpl in |- *; rewrite H9; right; simpl in |- *; replace s1 with t2. + simpl; rewrite H9; right; simpl; replace s1 with t2. assumption. simpl in H14; rewrite H14; rewrite Hyp_min; reflexivity. elim H8; intros; apply (H6 i). - simpl in |- *; apply lt_S_n; apply H1. + simpl; apply lt_S_n; apply H1. intros; rewrite H9; induction i as [| i Hreci]. - simpl in |- *; red in |- *; intro; elim Hyp_eq; apply Rle_antisym. - apply (H16 0%nat); simpl in |- *; apply lt_O_Sn. + simpl; red; intro; elim Hyp_eq; apply Rle_antisym. + apply (H16 0%nat); simpl; apply lt_O_Sn. rewrite <- Hyp_min; rewrite H6; simpl in H14; rewrite <- H14; right; reflexivity. elim H8; intros; rewrite <- H9; apply (H21 i); rewrite H9; rewrite H9 in H1; - simpl in |- *; simpl in H1; apply lt_S_n; apply H1. + simpl; simpl in H1; apply lt_S_n; apply H1. exists (cons t1 l'); exists (cons r1 (cons r2 lf')); rewrite H9 in H6; rewrite H3 in H1; unfold adapted_couple in H1, H6; decompose [and] H6; decompose [and] H1; clear H6 H1; - unfold adapted_couple_opt in |- *; unfold adapted_couple in |- *; + unfold adapted_couple_opt; unfold adapted_couple; repeat split. - rewrite H9; unfold ordered_Rlist in |- *; intros; simpl in H1; + rewrite H9; unfold ordered_Rlist; intros; simpl in H1; induction i as [| i Hreci]. - simpl in |- *; replace s1 with t2. - apply (H15 0%nat); simpl in |- *; apply lt_O_Sn. + simpl; replace s1 with t2. + apply (H15 0%nat); simpl; apply lt_O_Sn. simpl in H13; rewrite H13; rewrite Hyp_min; reflexivity. change (pos_Rl (cons s1 (cons s2 s3)) i <= pos_Rl (cons s1 (cons s2 s3)) (S i)) - in |- *; apply (H11 i); simpl in |- *; apply lt_S_n; + ; apply (H11 i); simpl; apply lt_S_n; assumption. - simpl in |- *; simpl in H18; apply H18. - rewrite H9; simpl in |- *; simpl in H12; rewrite H12; unfold Rmax in |- *; + simpl; simpl in H18; apply H18. + rewrite H9; simpl; simpl in H12; rewrite H12; unfold Rmax; case (Rle_dec t2 b); case (Rle_dec a b); intros; reflexivity || elim n; assumption. - rewrite H9; simpl in |- *; simpl in H14; rewrite H14; reflexivity. - intros; simpl in H1; unfold constant_D_eq, open_interval in |- *; intros; + rewrite H9; simpl; simpl in H14; rewrite H14; reflexivity. + intros; simpl in H1; unfold constant_D_eq, open_interval; intros; induction i as [| i Hreci]. - simpl in |- *; rewrite H9 in H6; simpl in H6; apply (H21 0%nat). - simpl in |- *; apply lt_O_Sn. - unfold open_interval in |- *; simpl in |- *; replace t2 with s1. + simpl; rewrite H9 in H6; simpl in H6; apply (H21 0%nat). + simpl; apply lt_O_Sn. + unfold open_interval; simpl; replace t2 with s1. assumption. simpl in H13; rewrite H13; rewrite Hyp_min; reflexivity. - change (f x = pos_Rl (cons r2 lf') i) in |- *; clear Hreci; apply (H16 i). - simpl in |- *; rewrite H9 in H1; simpl in H1; apply lt_S_n; apply H1. - rewrite H9 in H6; unfold open_interval in |- *; apply H6. + change (f x = pos_Rl (cons r2 lf') i); clear Hreci; apply (H16 i). + simpl; rewrite H9 in H1; simpl in H1; apply lt_S_n; apply H1. + rewrite H9 in H6; unfold open_interval; apply H6. intros; simpl in H1; induction i as [| i Hreci]. - simpl in |- *; left; assumption. + simpl; left; assumption. elim H8; intros; apply (H6 i). - simpl in |- *; apply lt_S_n; apply H1. + simpl; apply lt_S_n; apply H1. intros; rewrite H9; induction i as [| i Hreci]. - simpl in |- *; red in |- *; intro; elim Hyp_eq; apply Rle_antisym. - apply (H15 0%nat); simpl in |- *; apply lt_O_Sn. + simpl; red; intro; elim Hyp_eq; apply Rle_antisym. + apply (H15 0%nat); simpl; apply lt_O_Sn. rewrite <- Hyp_min; rewrite H6; simpl in H13; rewrite <- H13; right; reflexivity. elim H8; intros; rewrite <- H9; apply (H20 i); rewrite H9; rewrite H9 in H1; - simpl in |- *; simpl in H1; apply lt_S_n; apply H1. + simpl; simpl in H1; apply lt_S_n; apply H1. rewrite H3 in H1; clear H4; unfold adapted_couple in H1; decompose [and] H1; clear H1; clear H H7 H9; cut (Rmax a b = b); [ intro; rewrite H in H5; rewrite <- H5; apply RList_P7; - [ assumption | simpl in |- *; right; left; reflexivity ] - | unfold Rmax in |- *; case (Rle_dec a b); intro; + [ assumption | simpl; right; left; reflexivity ] + | unfold Rmax; case (Rle_dec a b); intro; [ reflexivity | elim n; assumption ] ]. Qed. @@ -536,7 +534,7 @@ Proof. simpl in H9; rewrite H9 in H16; cut (r1 <= Rmax a b). intro; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H17 H16)). rewrite <- H4; apply RList_P7; - [ assumption | simpl in |- *; right; left; reflexivity ]. + [ assumption | simpl; right; left; reflexivity ]. clear Hrecs3; induction lf2 as [| r5 lf2 Hreclf2]. simpl in H11; discriminate. clear Hreclf2; assert (H17 : r3 = r4). @@ -546,31 +544,31 @@ Proof. simpl in H18; rewrite <- (H17 x). rewrite <- (H18 x). reflexivity. - rewrite <- H12; unfold x in |- *; split. + rewrite <- H12; unfold x; split. apply Rmult_lt_reg_l with 2; [ prove_sup0 - | unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; + | unfold Rdiv; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym; [ rewrite Rmult_1_l; rewrite double; apply Rplus_lt_compat_l; assumption | discrR ] ]. apply Rmult_lt_reg_l with 2; [ prove_sup0 - | unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; + | unfold Rdiv; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym; [ rewrite Rmult_1_l; rewrite (Rplus_comm r); rewrite double; apply Rplus_lt_compat_l; assumption | discrR ] ]. - unfold x in |- *; split. + unfold x; split. apply Rmult_lt_reg_l with 2; [ prove_sup0 - | unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; + | unfold Rdiv; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym; [ rewrite Rmult_1_l; rewrite double; apply Rplus_lt_compat_l; assumption | discrR ] ]. apply Rlt_trans with s2; [ apply Rmult_lt_reg_l with 2; [ prove_sup0 - | unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); + | unfold Rdiv; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym; [ rewrite Rmult_1_l; rewrite (Rplus_comm r); rewrite double; apply Rplus_lt_compat_l; assumption @@ -578,8 +576,8 @@ Proof. | assumption ]. assert (H18 : f s2 = r3). apply (H8 0%nat); - [ simpl in |- *; apply lt_O_Sn - | unfold open_interval in |- *; simpl in |- *; split; assumption ]. + [ simpl; apply lt_O_Sn + | unfold open_interval; simpl; split; assumption ]. assert (H19 : r3 = r5). assert (H19 := H7 1%nat); simpl in H19; assert (H20 := H19 (lt_n_S _ _ (lt_O_Sn _))); elim H20; @@ -589,18 +587,18 @@ Proof. rewrite <- (H22 (lt_O_Sn _) x). rewrite <- (H23 (lt_n_S _ _ (lt_O_Sn _)) x). reflexivity. - unfold open_interval in |- *; simpl in |- *; unfold x in |- *; split. + unfold open_interval; simpl; unfold x; split. apply Rmult_lt_reg_l with 2; [ prove_sup0 - | unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; + | unfold Rdiv; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym; [ rewrite Rmult_1_l; rewrite double; apply Rplus_lt_compat_l; - unfold Rmin in |- *; case (Rle_dec r1 r0); intro; + unfold Rmin; case (Rle_dec r1 r0); intro; assumption | discrR ] ]. apply Rmult_lt_reg_l with 2; [ prove_sup0 - | unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; + | unfold Rdiv; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym; [ rewrite Rmult_1_l; rewrite double; apply Rlt_le_trans with (r0 + Rmin r1 r0); @@ -608,20 +606,20 @@ Proof. assumption | apply Rplus_le_compat_l; apply Rmin_r ] | discrR ] ]. - unfold open_interval in |- *; simpl in |- *; unfold x in |- *; split. + unfold open_interval; simpl; unfold x; split. apply Rlt_trans with s2; [ assumption | apply Rmult_lt_reg_l with 2; [ prove_sup0 - | unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); + | unfold Rdiv; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym; [ rewrite Rmult_1_l; rewrite double; apply Rplus_lt_compat_l; - unfold Rmin in |- *; case (Rle_dec r1 r0); + unfold Rmin; case (Rle_dec r1 r0); intro; assumption | discrR ] ] ]. apply Rmult_lt_reg_l with 2; [ prove_sup0 - | unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; + | unfold Rdiv; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym; [ rewrite Rmult_1_l; rewrite double; apply Rlt_le_trans with (r1 + Rmin r1 r0); @@ -638,20 +636,20 @@ Proof. | elim H24; rewrite <- H17; assumption ]. elim H2; clear H2; intros; assert (H17 := H16 0%nat); simpl in H17; elim (H17 (lt_O_Sn _)); assumption. - rewrite <- H0; rewrite H12; apply (H7 0%nat); simpl in |- *; apply lt_O_Sn. + rewrite <- H0; rewrite H12; apply (H7 0%nat); simpl; apply lt_O_Sn. Qed. Lemma StepFun_P12 : forall (a b:R) (f:R -> R) (l lf:Rlist), adapted_couple_opt f a b l lf -> adapted_couple_opt f b a l lf. Proof. - unfold adapted_couple_opt in |- *; unfold adapted_couple in |- *; intros; + unfold adapted_couple_opt; unfold adapted_couple; intros; decompose [and] H; clear H; repeat split; try assumption. - rewrite H0; unfold Rmin in |- *; case (Rle_dec a b); intro; + rewrite H0; unfold Rmin; case (Rle_dec a b); intro; case (Rle_dec b a); intro; try reflexivity. apply Rle_antisym; assumption. apply Rle_antisym; auto with real. - rewrite H3; unfold Rmax in |- *; case (Rle_dec a b); intro; + rewrite H3; unfold Rmax; case (Rle_dec a b); intro; case (Rle_dec b a); intro; try reflexivity. apply Rle_antisym; assumption. apply Rle_antisym; auto with real. @@ -691,10 +689,10 @@ Proof. case (Req_dec a b); intro. rewrite (StepFun_P8 H2 H4); rewrite (StepFun_P8 H H4); reflexivity. assert (Hyp_min : Rmin a b = a). - unfold Rmin in |- *; case (Rle_dec a b); intro; + unfold Rmin; case (Rle_dec a b); intro; [ reflexivity | elim n; assumption ]. assert (Hyp_max : Rmax a b = b). - unfold Rmax in |- *; case (Rle_dec a b); intro; + unfold Rmax; case (Rle_dec a b); intro; [ reflexivity | elim n; assumption ]. elim (RList_P20 _ (StepFun_P9 H H4)); intros s1 [s2 [s3 H5]]; rewrite H5 in H; rewrite H5; induction lf1 as [| r3 lf1 Hreclf1]. @@ -718,34 +716,34 @@ Proof. rewrite <- (H20 (lt_O_Sn _) x). reflexivity. assert (H21 := H13 0%nat (lt_O_Sn _)); simpl in H21; elim H21; intro; - [ idtac | elim H7; assumption ]; unfold x in |- *; + [ idtac | elim H7; assumption ]; unfold x; split. apply Rmult_lt_reg_l with 2; [ prove_sup0 - | unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; + | unfold Rdiv; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym; [ rewrite Rmult_1_l; rewrite double; apply Rplus_lt_compat_l; apply H | discrR ] ]. apply Rmult_lt_reg_l with 2; [ prove_sup0 - | unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; + | unfold Rdiv; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym; [ rewrite Rmult_1_l; rewrite <- (Rplus_comm r1); rewrite double; apply Rplus_lt_compat_l; apply H | discrR ] ]. rewrite <- H6; assert (H21 := H13 0%nat (lt_O_Sn _)); simpl in H21; elim H21; - intro; [ idtac | elim H7; assumption ]; unfold x in |- *; + intro; [ idtac | elim H7; assumption ]; unfold x; split. apply Rmult_lt_reg_l with 2; [ prove_sup0 - | unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; + | unfold Rdiv; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym; [ rewrite Rmult_1_l; rewrite double; apply Rplus_lt_compat_l; apply H | discrR ] ]. apply Rlt_le_trans with r1; [ apply Rmult_lt_reg_l with 2; [ prove_sup0 - | unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); + | unfold Rdiv; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym; [ rewrite Rmult_1_l; rewrite <- (Rplus_comm r1); rewrite double; apply Rplus_lt_compat_l; apply H @@ -754,64 +752,64 @@ Proof. eapply StepFun_P13. apply H4. apply H2. - unfold adapted_couple_opt in |- *; split. + unfold adapted_couple_opt; split. apply H. rewrite H5 in H3; apply H3. assert (H8 : r1 <= s2). eapply StepFun_P13. apply H4. apply H2. - unfold adapted_couple_opt in |- *; split. + unfold adapted_couple_opt; split. apply H. rewrite H5 in H3; apply H3. elim H7; intro. - simpl in |- *; elim H8; intro. + simpl; elim H8; intro. replace (r4 * (s2 - s1)) with (r3 * (r1 - r) + r3 * (s2 - r1)); [ idtac | rewrite H9; rewrite H6; ring ]. rewrite Rplus_assoc; apply Rplus_eq_compat_l; change (Int_SF lf1 (cons r1 r2) = Int_SF (cons r3 lf2) (cons r1 (cons s2 s3))) - in |- *; apply H0 with r1 b. + ; apply H0 with r1 b. unfold adapted_couple in H2; decompose [and] H2; clear H2; replace b with (Rmax a b). rewrite <- H12; apply RList_P7; - [ assumption | simpl in |- *; right; left; reflexivity ]. + [ assumption | simpl; right; left; reflexivity ]. eapply StepFun_P7. apply H1. apply H2. - unfold adapted_couple_opt in |- *; split. + unfold adapted_couple_opt; split. apply StepFun_P7 with a a r3. apply H1. unfold adapted_couple in H2, H; decompose [and] H2; decompose [and] H; clear H H2; assert (H20 : r = a). simpl in H13; rewrite H13; apply Hyp_min. - unfold adapted_couple in |- *; repeat split. - unfold ordered_Rlist in |- *; intros; simpl in H; induction i as [| i Hreci]. - simpl in |- *; rewrite <- H20; apply (H11 0%nat). - simpl in |- *; apply lt_O_Sn. + unfold adapted_couple; repeat split. + unfold ordered_Rlist; intros; simpl in H; induction i as [| i Hreci]. + simpl; rewrite <- H20; apply (H11 0%nat). + simpl; apply lt_O_Sn. induction i as [| i Hreci0]. - simpl in |- *; assumption. - change (pos_Rl (cons s2 s3) i <= pos_Rl (cons s2 s3) (S i)) in |- *; - apply (H15 (S i)); simpl in |- *; apply lt_S_n; assumption. - simpl in |- *; symmetry in |- *; apply Hyp_min. + simpl; assumption. + change (pos_Rl (cons s2 s3) i <= pos_Rl (cons s2 s3) (S i)); + apply (H15 (S i)); simpl; apply lt_S_n; assumption. + simpl; symmetry ; apply Hyp_min. rewrite <- H17; reflexivity. - simpl in H19; simpl in |- *; rewrite H19; reflexivity. - intros; simpl in H; unfold constant_D_eq, open_interval in |- *; intros; + simpl in H19; simpl; rewrite H19; reflexivity. + intros; simpl in H; unfold constant_D_eq, open_interval; intros; induction i as [| i Hreci]. - simpl in |- *; apply (H16 0%nat). - simpl in |- *; apply lt_O_Sn. - simpl in H2; rewrite <- H20 in H2; unfold open_interval in |- *; - simpl in |- *; apply H2. + simpl; apply (H16 0%nat). + simpl; apply lt_O_Sn. + simpl in H2; rewrite <- H20 in H2; unfold open_interval; + simpl; apply H2. clear Hreci; induction i as [| i Hreci]. - simpl in |- *; simpl in H2; rewrite H9; apply (H21 0%nat). - simpl in |- *; apply lt_O_Sn. - unfold open_interval in |- *; simpl in |- *; elim H2; intros; split. + simpl; simpl in H2; rewrite H9; apply (H21 0%nat). + simpl; apply lt_O_Sn. + unfold open_interval; simpl; elim H2; intros; split. apply Rle_lt_trans with r1; try assumption; rewrite <- H6; apply (H11 0%nat); - simpl in |- *; apply lt_O_Sn. + simpl; apply lt_O_Sn. assumption. - clear Hreci; simpl in |- *; apply (H21 (S i)). - simpl in |- *; apply lt_S_n; assumption. - unfold open_interval in |- *; apply H2. + clear Hreci; simpl; apply (H21 (S i)). + simpl; apply lt_S_n; assumption. + unfold open_interval; apply H2. elim H3; clear H3; intros; split. rewrite H9; change @@ -819,64 +817,64 @@ Proof. (i < pred (Rlength (cons r4 lf2)))%nat -> pos_Rl (cons r4 lf2) i <> pos_Rl (cons r4 lf2) (S i) \/ f (pos_Rl (cons s1 (cons s2 s3)) (S i)) <> pos_Rl (cons r4 lf2) i) - in |- *; rewrite <- H5; apply H3. + ; rewrite <- H5; apply H3. rewrite H5 in H11; intros; simpl in H12; induction i as [| i Hreci]. - simpl in |- *; red in |- *; intro; rewrite H13 in H10; + simpl; red; intro; rewrite H13 in H10; elim (Rlt_irrefl _ H10). - clear Hreci; apply (H11 (S i)); simpl in |- *; apply H12. + clear Hreci; apply (H11 (S i)); simpl; apply H12. rewrite H9; rewrite H10; rewrite H6; apply Rplus_eq_compat_l; rewrite <- H10; apply H0 with r1 b. unfold adapted_couple in H2; decompose [and] H2; clear H2; replace b with (Rmax a b). rewrite <- H12; apply RList_P7; - [ assumption | simpl in |- *; right; left; reflexivity ]. + [ assumption | simpl; right; left; reflexivity ]. eapply StepFun_P7. apply H1. apply H2. - unfold adapted_couple_opt in |- *; split. + unfold adapted_couple_opt; split. apply StepFun_P7 with a a r3. apply H1. unfold adapted_couple in H2, H; decompose [and] H2; decompose [and] H; clear H H2; assert (H20 : r = a). simpl in H13; rewrite H13; apply Hyp_min. - unfold adapted_couple in |- *; repeat split. - unfold ordered_Rlist in |- *; intros; simpl in H; induction i as [| i Hreci]. - simpl in |- *; rewrite <- H20; apply (H11 0%nat); simpl in |- *; + unfold adapted_couple; repeat split. + unfold ordered_Rlist; intros; simpl in H; induction i as [| i Hreci]. + simpl; rewrite <- H20; apply (H11 0%nat); simpl; apply lt_O_Sn. - rewrite H10; apply (H15 (S i)); simpl in |- *; assumption. - simpl in |- *; symmetry in |- *; apply Hyp_min. + rewrite H10; apply (H15 (S i)); simpl; assumption. + simpl; symmetry ; apply Hyp_min. rewrite <- H17; rewrite H10; reflexivity. - simpl in H19; simpl in |- *; apply H19. - intros; simpl in H; unfold constant_D_eq, open_interval in |- *; intros; + simpl in H19; simpl; apply H19. + intros; simpl in H; unfold constant_D_eq, open_interval; intros; induction i as [| i Hreci]. - simpl in |- *; apply (H16 0%nat). - simpl in |- *; apply lt_O_Sn. - simpl in H2; rewrite <- H20 in H2; unfold open_interval in |- *; - simpl in |- *; apply H2. - clear Hreci; simpl in |- *; apply (H21 (S i)). - simpl in |- *; assumption. - rewrite <- H10; unfold open_interval in |- *; apply H2. + simpl; apply (H16 0%nat). + simpl; apply lt_O_Sn. + simpl in H2; rewrite <- H20 in H2; unfold open_interval; + simpl; apply H2. + clear Hreci; simpl; apply (H21 (S i)). + simpl; assumption. + rewrite <- H10; unfold open_interval; apply H2. elim H3; clear H3; intros; split. rewrite H5 in H3; intros; apply (H3 (S i)). - simpl in |- *; replace (Rlength lf2) with (S (pred (Rlength lf2))). + simpl; replace (Rlength lf2) with (S (pred (Rlength lf2))). apply lt_n_S; apply H12. - symmetry in |- *; apply S_pred with 0%nat; apply neq_O_lt; red in |- *; + symmetry ; apply S_pred with 0%nat; apply neq_O_lt; red; intro; rewrite <- H13 in H12; elim (lt_n_O _ H12). intros; simpl in H12; rewrite H10; rewrite H5 in H11; apply (H11 (S i)); - simpl in |- *; apply lt_n_S; apply H12. - simpl in |- *; rewrite H9; unfold Rminus in |- *; rewrite Rplus_opp_r; + simpl; apply lt_n_S; apply H12. + simpl; rewrite H9; unfold Rminus; rewrite Rplus_opp_r; rewrite Rmult_0_r; rewrite Rplus_0_l; change (Int_SF lf1 (cons r1 r2) = Int_SF (cons r4 lf2) (cons s1 (cons s2 s3))) - in |- *; eapply H0. + ; eapply H0. apply H1. - 2: rewrite H5 in H3; unfold adapted_couple_opt in |- *; split; assumption. + 2: rewrite H5 in H3; unfold adapted_couple_opt; split; assumption. assert (H10 : r = a). unfold adapted_couple in H2; decompose [and] H2; clear H2; simpl in H12; rewrite H12; apply Hyp_min. rewrite <- H9; rewrite H10; apply StepFun_P7 with a r r3; [ apply H1 - | pattern a at 2 in |- *; rewrite <- H10; pattern r at 2 in |- *; rewrite H9; + | pattern a at 2; rewrite <- H10; pattern r at 2; rewrite H9; apply H2 ]. Qed. @@ -920,12 +918,12 @@ Qed. Lemma StepFun_P18 : forall a b c:R, RiemannInt_SF (mkStepFun (StepFun_P4 a b c)) = c * (b - a). Proof. - intros; unfold RiemannInt_SF in |- *; case (Rle_dec a b); intro. + intros; unfold RiemannInt_SF; case (Rle_dec a b); intro. replace (Int_SF (subdivision_val (mkStepFun (StepFun_P4 a b c))) (subdivision (mkStepFun (StepFun_P4 a b c)))) with (Int_SF (cons c nil) (cons a (cons b nil))); - [ simpl in |- *; ring + [ simpl; ring | apply StepFun_P17 with (fct_cte c) a b; [ apply StepFun_P3; assumption | apply (StepFun_P1 (mkStepFun (StepFun_P4 a b c))) ] ]. @@ -933,7 +931,7 @@ Proof. (Int_SF (subdivision_val (mkStepFun (StepFun_P4 a b c))) (subdivision (mkStepFun (StepFun_P4 a b c)))) with (Int_SF (cons c nil) (cons b (cons a nil))); - [ simpl in |- *; ring + [ simpl; ring | apply StepFun_P17 with (fct_cte c) a b; [ apply StepFun_P2; apply StepFun_P3; auto with real | apply (StepFun_P1 (mkStepFun (StepFun_P4 a b c))) ] ]. @@ -945,8 +943,8 @@ Lemma StepFun_P19 : Int_SF (FF l1 f) l1 + l * Int_SF (FF l1 g) l1. Proof. intros; induction l1 as [| r l1 Hrecl1]; - [ simpl in |- *; ring - | induction l1 as [| r0 l1 Hrecl0]; simpl in |- *; + [ simpl; ring + | induction l1 as [| r0 l1 Hrecl0]; simpl; [ ring | simpl in Hrecl1; rewrite Hrecl1; ring ] ]. Qed. @@ -956,38 +954,38 @@ Lemma StepFun_P20 : Proof. intros l f H; induction l; [ elim (lt_irrefl _ H) - | simpl in |- *; rewrite RList_P18; rewrite RList_P14; reflexivity ]. + | simpl; rewrite RList_P18; rewrite RList_P14; reflexivity ]. Qed. Lemma StepFun_P21 : forall (a b:R) (f:R -> R) (l:Rlist), is_subdivision f a b l -> adapted_couple f a b l (FF l f). Proof. - intros; unfold adapted_couple in |- *; unfold is_subdivision in X; + intros; unfold adapted_couple; unfold is_subdivision in X; unfold adapted_couple in X; elim X; clear X; intros; decompose [and] p; clear p; repeat split; try assumption. apply StepFun_P20; rewrite H2; apply lt_O_Sn. intros; assert (H5 := H4 _ H3); unfold constant_D_eq, open_interval in H5; - unfold constant_D_eq, open_interval in |- *; intros; + unfold constant_D_eq, open_interval; intros; induction l as [| r l Hrecl]. discriminate. - unfold FF in |- *; rewrite RList_P12. - simpl in |- *; - change (f x0 = f (pos_Rl (mid_Rlist (cons r l) r) (S i))) in |- *; + unfold FF; rewrite RList_P12. + simpl; + change (f x0 = f (pos_Rl (mid_Rlist (cons r l) r) (S i))); rewrite RList_P13; try assumption; rewrite (H5 x0 H6); rewrite H5. reflexivity. split. apply Rmult_lt_reg_l with 2; [ prove_sup0 - | unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; + | unfold Rdiv; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym; [ rewrite Rmult_1_l; rewrite double; apply Rplus_lt_compat_l; elim H6; intros; apply Rlt_trans with x0; assumption | discrR ] ]. apply Rmult_lt_reg_l with 2; [ prove_sup0 - | unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; + | unfold Rdiv; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym; [ rewrite Rmult_1_l; rewrite double; rewrite (Rplus_comm (pos_Rl (cons r l) i)); @@ -1003,22 +1001,22 @@ Lemma StepFun_P22 : is_subdivision f a b lf -> is_subdivision g a b lg -> is_subdivision f a b (cons_ORlist lf lg). Proof. - unfold is_subdivision in |- *; intros a b f g lf lg Hyp X X0; elim X; elim X0; + unfold is_subdivision; intros a b f g lf lg Hyp X X0; elim X; elim X0; clear X X0; intros lg0 p lf0 p0; assert (Hyp_min : Rmin a b = a). - unfold Rmin in |- *; case (Rle_dec a b); intro; + unfold Rmin; case (Rle_dec a b); intro; [ reflexivity | elim n; assumption ]. assert (Hyp_max : Rmax a b = b). - unfold Rmax in |- *; case (Rle_dec a b); intro; + unfold Rmax; case (Rle_dec a b); intro; [ reflexivity | elim n; assumption ]. apply existT with (FF (cons_ORlist lf lg) f); unfold adapted_couple in p, p0; decompose [and] p; decompose [and] p0; clear p p0; rewrite Hyp_min in H6; rewrite Hyp_min in H1; rewrite Hyp_max in H0; - rewrite Hyp_max in H5; unfold adapted_couple in |- *; + rewrite Hyp_max in H5; unfold adapted_couple; repeat split. apply RList_P2; assumption. - rewrite Hyp_min; symmetry in |- *; apply Rle_antisym. + rewrite Hyp_min; symmetry ; apply Rle_antisym. induction lf as [| r lf Hreclf]. - simpl in |- *; right; symmetry in |- *; assumption. + simpl; right; symmetry ; assumption. assert (H10 : In (pos_Rl (cons_ORlist (cons r lf) lg) 0) (cons_ORlist (cons r lf) lg)). @@ -1026,7 +1024,7 @@ Proof. (RList_P3 (cons_ORlist (cons r lf) lg) (pos_Rl (cons_ORlist (cons r lf) lg) 0)); intros _ H10; apply H10; exists 0%nat; split; - [ reflexivity | rewrite RList_P11; simpl in |- *; apply lt_O_Sn ]. + [ reflexivity | rewrite RList_P11; simpl; apply lt_O_Sn ]. elim (RList_P9 (cons r lf) lg (pos_Rl (cons_ORlist (cons r lf) lg) 0)); intros H12 _; assert (H13 := H12 H10); elim H13; intro. elim (RList_P3 (cons r lf) (pos_Rl (cons_ORlist (cons r lf) lg) 0)); @@ -1039,16 +1037,16 @@ Proof. clear H15; intros; rewrite H15; rewrite <- H1; elim (RList_P6 lg); intros; apply H17; [ assumption | apply le_O_n | assumption ]. induction lf as [| r lf Hreclf]. - simpl in |- *; right; assumption. + simpl; right; assumption. assert (H8 : In a (cons_ORlist (cons r lf) lg)). elim (RList_P9 (cons r lf) lg a); intros; apply H10; left; elim (RList_P3 (cons r lf) a); intros; apply H12; exists 0%nat; split; - [ symmetry in |- *; assumption | simpl in |- *; apply lt_O_Sn ]. + [ symmetry ; assumption | simpl; apply lt_O_Sn ]. apply RList_P5; [ apply RList_P2; assumption | assumption ]. rewrite Hyp_max; apply Rle_antisym. induction lf as [| r lf Hreclf]. - simpl in |- *; right; assumption. + simpl; right; assumption. assert (H8 : In @@ -1061,7 +1059,7 @@ Proof. (pred (Rlength (cons_ORlist (cons r lf) lg))))); intros _ H10; apply H10; exists (pred (Rlength (cons_ORlist (cons r lf) lg))); - split; [ reflexivity | rewrite RList_P11; simpl in |- *; apply lt_n_Sn ]. + split; [ reflexivity | rewrite RList_P11; simpl; apply lt_n_Sn ]. elim (RList_P9 (cons r lf) lg (pos_Rl (cons_ORlist (cons r lf) lg) @@ -1076,8 +1074,8 @@ Proof. elim H15; clear H15; intros; rewrite H15; rewrite <- H5; elim (RList_P6 (cons r lf)); intros; apply H17; [ assumption - | simpl in |- *; simpl in H14; apply lt_n_Sm_le; assumption - | simpl in |- *; apply lt_n_Sn ]. + | simpl; simpl in H14; apply lt_n_Sm_le; assumption + | simpl; apply lt_n_Sn ]. elim (RList_P3 lg (pos_Rl (cons_ORlist (cons r lf) lg) @@ -1085,23 +1083,23 @@ Proof. intros H13 _; assert (H14 := H13 H12); elim H14; intros; elim H15; clear H15; intros. rewrite H15; assert (H17 : Rlength lg = S (pred (Rlength lg))). - apply S_pred with 0%nat; apply neq_O_lt; red in |- *; intro; + apply S_pred with 0%nat; apply neq_O_lt; red; intro; rewrite <- H17 in H16; elim (lt_n_O _ H16). rewrite <- H0; elim (RList_P6 lg); intros; apply H18; [ assumption | rewrite H17 in H16; apply lt_n_Sm_le; assumption | apply lt_pred_n_n; rewrite H17; apply lt_O_Sn ]. induction lf as [| r lf Hreclf]. - simpl in |- *; right; symmetry in |- *; assumption. + simpl; right; symmetry ; assumption. assert (H8 : In b (cons_ORlist (cons r lf) lg)). elim (RList_P9 (cons r lf) lg b); intros; apply H10; left; elim (RList_P3 (cons r lf) b); intros; apply H12; exists (pred (Rlength (cons r lf))); split; - [ symmetry in |- *; assumption | simpl in |- *; apply lt_n_Sn ]. + [ symmetry ; assumption | simpl; apply lt_n_Sn ]. apply RList_P7; [ apply RList_P2; assumption | assumption ]. - apply StepFun_P20; rewrite RList_P11; rewrite H2; rewrite H7; simpl in |- *; + apply StepFun_P20; rewrite RList_P11; rewrite H2; rewrite H7; simpl; apply lt_O_Sn. - intros; unfold constant_D_eq, open_interval in |- *; intros; + intros; unfold constant_D_eq, open_interval; intros; cut (exists l : R, constant_D_eq f @@ -1111,10 +1109,10 @@ Proof. assert (Hyp_cons : exists r : R, (exists r0 : Rlist, cons_ORlist lf lg = cons r r0)). - apply RList_P19; red in |- *; intro; rewrite H13 in H8; elim (lt_n_O _ H8). + apply RList_P19; red; intro; rewrite H13 in H8; elim (lt_n_O _ H8). elim Hyp_cons; clear Hyp_cons; intros r [r0 Hyp_cons]; rewrite Hyp_cons; - unfold FF in |- *; rewrite RList_P12. - change (f x = f (pos_Rl (mid_Rlist (cons r r0) r) (S i))) in |- *; + unfold FF; rewrite RList_P12. + change (f x = f (pos_Rl (mid_Rlist (cons r r0) r) (S i))); rewrite <- Hyp_cons; rewrite RList_P13. assert (H13 := RList_P2 _ _ H _ H8); elim H13; intro. unfold constant_D_eq, open_interval in H11, H12; rewrite (H11 x H10); @@ -1126,13 +1124,13 @@ Proof. split. apply Rmult_lt_reg_l with 2; [ prove_sup0 - | unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; + | unfold Rdiv; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym; [ rewrite Rmult_1_l; rewrite double; apply Rplus_lt_compat_l; assumption | discrR ] ]. apply Rmult_lt_reg_l with 2; [ prove_sup0 - | unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; + | unfold Rdiv; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym; [ rewrite Rmult_1_l; rewrite double; rewrite (Rplus_comm (pos_Rl (cons_ORlist lf lg) i)); @@ -1151,7 +1149,7 @@ Proof. apply le_O_n. apply lt_trans with (pred (Rlength (cons_ORlist lf lg))); [ assumption - | apply lt_pred_n_n; apply neq_O_lt; red in |- *; intro; + | apply lt_pred_n_n; apply neq_O_lt; red; intro; rewrite <- H13 in H8; elim (lt_n_O _ H8) ]. assumption. assumption. @@ -1162,7 +1160,7 @@ Proof. elim (RList_P6 (cons_ORlist lf lg)); intros; apply H11. apply RList_P2; assumption. apply lt_n_Sm_le; apply lt_n_S; assumption. - apply lt_pred_n_n; apply neq_O_lt; red in |- *; intro; rewrite <- H13 in H8; + apply lt_pred_n_n; apply neq_O_lt; red; intro; rewrite <- H13 in H8; elim (lt_n_O _ H8). rewrite H0; assumption. set @@ -1170,24 +1168,24 @@ Proof. fun j:nat => pos_Rl lf j <= pos_Rl (cons_ORlist lf lg) i /\ (j < Rlength lf)%nat); assert (H12 : Nbound I). - unfold Nbound in |- *; exists (Rlength lf); intros; unfold I in H12; elim H12; + unfold Nbound; exists (Rlength lf); intros; unfold I in H12; elim H12; intros; apply lt_le_weak; assumption. assert (H13 : exists n : nat, I n). - exists 0%nat; unfold I in |- *; split. + exists 0%nat; unfold I; split. apply Rle_trans with (pos_Rl (cons_ORlist lf lg) 0). - right; symmetry in |- *. + right; symmetry . apply RList_P15; try assumption; rewrite H1; assumption. elim (RList_P6 (cons_ORlist lf lg)); intros; apply H13. apply RList_P2; assumption. apply le_O_n. apply lt_trans with (pred (Rlength (cons_ORlist lf lg))). assumption. - apply lt_pred_n_n; apply neq_O_lt; red in |- *; intro; rewrite <- H15 in H8; + apply lt_pred_n_n; apply neq_O_lt; red; intro; rewrite <- H15 in H8; elim (lt_n_O _ H8). - apply neq_O_lt; red in |- *; intro; rewrite <- H13 in H5; + apply neq_O_lt; red; intro; rewrite <- H13 in H5; rewrite <- H6 in H11; rewrite <- H5 in H11; elim (Rlt_irrefl _ H11). assert (H14 := Nzorn H13 H12); elim H14; clear H14; intros x0 H14; - exists (pos_Rl lf0 x0); unfold constant_D_eq, open_interval in |- *; + exists (pos_Rl lf0 x0); unfold constant_D_eq, open_interval; intros; assert (H16 := H9 x0); assert (H17 : (x0 < pred (Rlength lf))%nat). elim H14; clear H14; intros; unfold I in H14; elim H14; clear H14; intros; apply lt_S_n; replace (S (pred (Rlength lf))) with (Rlength lf). @@ -1205,11 +1203,11 @@ Proof. elim (RList_P6 (cons_ORlist lf lg)); intros; apply H21. apply RList_P2; assumption. apply lt_n_Sm_le; apply lt_n_S; assumption. - apply lt_pred_n_n; apply neq_O_lt; red in |- *; intro; rewrite <- H23 in H8; + apply lt_pred_n_n; apply neq_O_lt; red; intro; rewrite <- H23 in H8; elim (lt_n_O _ H8). right; apply RList_P16; try assumption; rewrite H0; assumption. rewrite <- H20; reflexivity. - apply S_pred with 0%nat; apply neq_O_lt; red in |- *; intro; + apply S_pred with 0%nat; apply neq_O_lt; red; intro; rewrite <- H19 in H18; elim (lt_n_O _ H18). assert (H18 := H16 H17); unfold constant_D_eq, open_interval in H18; rewrite (H18 x1). @@ -1221,11 +1219,11 @@ Proof. assert (H22 : (S x0 < Rlength lf)%nat). replace (Rlength lf) with (S (pred (Rlength lf))); [ apply lt_n_S; assumption - | symmetry in |- *; apply S_pred with 0%nat; apply neq_O_lt; red in |- *; + | symmetry ; apply S_pred with 0%nat; apply neq_O_lt; red; intro; rewrite <- H22 in H21; elim (lt_n_O _ H21) ]. elim (Rle_dec (pos_Rl lf (S x0)) (pos_Rl (cons_ORlist lf lg) i)); intro. assert (H23 : (S x0 <= x0)%nat). - apply H20; unfold I in |- *; split; assumption. + apply H20; unfold I; split; assumption. elim (le_Sn_n _ H23). assert (H23 : pos_Rl (cons_ORlist lf lg) i < pos_Rl lf (S x0)). auto with real. @@ -1255,22 +1253,22 @@ Lemma StepFun_P24 : is_subdivision f a b lf -> is_subdivision g a b lg -> is_subdivision g a b (cons_ORlist lf lg). Proof. - unfold is_subdivision in |- *; intros a b f g lf lg Hyp X X0; elim X; elim X0; + unfold is_subdivision; intros a b f g lf lg Hyp X X0; elim X; elim X0; clear X X0; intros lg0 p lf0 p0; assert (Hyp_min : Rmin a b = a). - unfold Rmin in |- *; case (Rle_dec a b); intro; + unfold Rmin; case (Rle_dec a b); intro; [ reflexivity | elim n; assumption ]. assert (Hyp_max : Rmax a b = b). - unfold Rmax in |- *; case (Rle_dec a b); intro; + unfold Rmax; case (Rle_dec a b); intro; [ reflexivity | elim n; assumption ]. apply existT with (FF (cons_ORlist lf lg) g); unfold adapted_couple in p, p0; decompose [and] p; decompose [and] p0; clear p p0; rewrite Hyp_min in H1; rewrite Hyp_min in H6; rewrite Hyp_max in H0; - rewrite Hyp_max in H5; unfold adapted_couple in |- *; + rewrite Hyp_max in H5; unfold adapted_couple; repeat split. apply RList_P2; assumption. - rewrite Hyp_min; symmetry in |- *; apply Rle_antisym. + rewrite Hyp_min; symmetry ; apply Rle_antisym. induction lf as [| r lf Hreclf]. - simpl in |- *; right; symmetry in |- *; assumption. + simpl; right; symmetry ; assumption. assert (H10 : In (pos_Rl (cons_ORlist (cons r lf) lg) 0) (cons_ORlist (cons r lf) lg)). @@ -1278,7 +1276,7 @@ Proof. (RList_P3 (cons_ORlist (cons r lf) lg) (pos_Rl (cons_ORlist (cons r lf) lg) 0)); intros _ H10; apply H10; exists 0%nat; split; - [ reflexivity | rewrite RList_P11; simpl in |- *; apply lt_O_Sn ]. + [ reflexivity | rewrite RList_P11; simpl; apply lt_O_Sn ]. elim (RList_P9 (cons r lf) lg (pos_Rl (cons_ORlist (cons r lf) lg) 0)); intros H12 _; assert (H13 := H12 H10); elim H13; intro. elim (RList_P3 (cons r lf) (pos_Rl (cons_ORlist (cons r lf) lg) 0)); @@ -1291,16 +1289,16 @@ Proof. clear H15; intros; rewrite H15; rewrite <- H1; elim (RList_P6 lg); intros; apply H17; [ assumption | apply le_O_n | assumption ]. induction lf as [| r lf Hreclf]. - simpl in |- *; right; assumption. + simpl; right; assumption. assert (H8 : In a (cons_ORlist (cons r lf) lg)). elim (RList_P9 (cons r lf) lg a); intros; apply H10; left; elim (RList_P3 (cons r lf) a); intros; apply H12; exists 0%nat; split; - [ symmetry in |- *; assumption | simpl in |- *; apply lt_O_Sn ]. + [ symmetry ; assumption | simpl; apply lt_O_Sn ]. apply RList_P5; [ apply RList_P2; assumption | assumption ]. rewrite Hyp_max; apply Rle_antisym. induction lf as [| r lf Hreclf]. - simpl in |- *; right; assumption. + simpl; right; assumption. assert (H8 : In @@ -1313,7 +1311,7 @@ Proof. (pred (Rlength (cons_ORlist (cons r lf) lg))))); intros _ H10; apply H10; exists (pred (Rlength (cons_ORlist (cons r lf) lg))); - split; [ reflexivity | rewrite RList_P11; simpl in |- *; apply lt_n_Sn ]. + split; [ reflexivity | rewrite RList_P11; simpl; apply lt_n_Sn ]. elim (RList_P9 (cons r lf) lg (pos_Rl (cons_ORlist (cons r lf) lg) @@ -1327,8 +1325,8 @@ Proof. elim H15; clear H15; intros; rewrite H15; rewrite <- H5; elim (RList_P6 (cons r lf)); intros; apply H17; [ assumption - | simpl in |- *; simpl in H14; apply lt_n_Sm_le; assumption - | simpl in |- *; apply lt_n_Sn ]. + | simpl; simpl in H14; apply lt_n_Sm_le; assumption + | simpl; apply lt_n_Sn ]. elim (RList_P3 lg (pos_Rl (cons_ORlist (cons r lf) lg) @@ -1336,23 +1334,23 @@ Proof. intros H13 _; assert (H14 := H13 H12); elim H14; intros; elim H15; clear H15; intros; rewrite H15; assert (H17 : Rlength lg = S (pred (Rlength lg))). - apply S_pred with 0%nat; apply neq_O_lt; red in |- *; intro; + apply S_pred with 0%nat; apply neq_O_lt; red; intro; rewrite <- H17 in H16; elim (lt_n_O _ H16). rewrite <- H0; elim (RList_P6 lg); intros; apply H18; [ assumption | rewrite H17 in H16; apply lt_n_Sm_le; assumption | apply lt_pred_n_n; rewrite H17; apply lt_O_Sn ]. induction lf as [| r lf Hreclf]. - simpl in |- *; right; symmetry in |- *; assumption. + simpl; right; symmetry ; assumption. assert (H8 : In b (cons_ORlist (cons r lf) lg)). elim (RList_P9 (cons r lf) lg b); intros; apply H10; left; elim (RList_P3 (cons r lf) b); intros; apply H12; exists (pred (Rlength (cons r lf))); split; - [ symmetry in |- *; assumption | simpl in |- *; apply lt_n_Sn ]. + [ symmetry ; assumption | simpl; apply lt_n_Sn ]. apply RList_P7; [ apply RList_P2; assumption | assumption ]. - apply StepFun_P20; rewrite RList_P11; rewrite H7; rewrite H2; simpl in |- *; + apply StepFun_P20; rewrite RList_P11; rewrite H7; rewrite H2; simpl; apply lt_O_Sn. - unfold constant_D_eq, open_interval in |- *; intros; + unfold constant_D_eq, open_interval; intros; cut (exists l : R, constant_D_eq g @@ -1362,10 +1360,10 @@ Proof. assert (Hyp_cons : exists r : R, (exists r0 : Rlist, cons_ORlist lf lg = cons r r0)). - apply RList_P19; red in |- *; intro; rewrite H13 in H8; elim (lt_n_O _ H8). + apply RList_P19; red; intro; rewrite H13 in H8; elim (lt_n_O _ H8). elim Hyp_cons; clear Hyp_cons; intros r [r0 Hyp_cons]; rewrite Hyp_cons; - unfold FF in |- *; rewrite RList_P12. - change (g x = g (pos_Rl (mid_Rlist (cons r r0) r) (S i))) in |- *; + unfold FF; rewrite RList_P12. + change (g x = g (pos_Rl (mid_Rlist (cons r r0) r) (S i))); rewrite <- Hyp_cons; rewrite RList_P13. assert (H13 := RList_P2 _ _ H _ H8); elim H13; intro. unfold constant_D_eq, open_interval in H11, H12; rewrite (H11 x H10); @@ -1377,13 +1375,13 @@ Proof. split. apply Rmult_lt_reg_l with 2; [ prove_sup0 - | unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; + | unfold Rdiv; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym; [ rewrite Rmult_1_l; rewrite double; apply Rplus_lt_compat_l; assumption | discrR ] ]. apply Rmult_lt_reg_l with 2; [ prove_sup0 - | unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; + | unfold Rdiv; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym; [ rewrite Rmult_1_l; rewrite double; rewrite (Rplus_comm (pos_Rl (cons_ORlist lf lg) i)); @@ -1402,7 +1400,7 @@ Proof. apply le_O_n. apply lt_trans with (pred (Rlength (cons_ORlist lf lg))); [ assumption - | apply lt_pred_n_n; apply neq_O_lt; red in |- *; intro; + | apply lt_pred_n_n; apply neq_O_lt; red; intro; rewrite <- H13 in H8; elim (lt_n_O _ H8) ]. rewrite H1; assumption. apply Rlt_le_trans with (pos_Rl (cons_ORlist lf lg) (S i)). @@ -1411,7 +1409,7 @@ Proof. elim (RList_P6 (cons_ORlist lf lg)); intros; apply H11. apply RList_P2; assumption. apply lt_n_Sm_le; apply lt_n_S; assumption. - apply lt_pred_n_n; apply neq_O_lt; red in |- *; intro; rewrite <- H13 in H8; + apply lt_pred_n_n; apply neq_O_lt; red; intro; rewrite <- H13 in H8; elim (lt_n_O _ H8). rewrite H0; assumption. set @@ -1419,24 +1417,24 @@ Proof. fun j:nat => pos_Rl lg j <= pos_Rl (cons_ORlist lf lg) i /\ (j < Rlength lg)%nat); assert (H12 : Nbound I). - unfold Nbound in |- *; exists (Rlength lg); intros; unfold I in H12; elim H12; + unfold Nbound; exists (Rlength lg); intros; unfold I in H12; elim H12; intros; apply lt_le_weak; assumption. assert (H13 : exists n : nat, I n). - exists 0%nat; unfold I in |- *; split. + exists 0%nat; unfold I; split. apply Rle_trans with (pos_Rl (cons_ORlist lf lg) 0). - right; symmetry in |- *; rewrite H1; rewrite <- H6; apply RList_P15; + right; symmetry ; rewrite H1; rewrite <- H6; apply RList_P15; try assumption; rewrite H1; assumption. elim (RList_P6 (cons_ORlist lf lg)); intros; apply H13; [ apply RList_P2; assumption | apply le_O_n | apply lt_trans with (pred (Rlength (cons_ORlist lf lg))); [ assumption - | apply lt_pred_n_n; apply neq_O_lt; red in |- *; intro; + | apply lt_pred_n_n; apply neq_O_lt; red; intro; rewrite <- H15 in H8; elim (lt_n_O _ H8) ] ]. - apply neq_O_lt; red in |- *; intro; rewrite <- H13 in H0; + apply neq_O_lt; red; intro; rewrite <- H13 in H0; rewrite <- H1 in H11; rewrite <- H0 in H11; elim (Rlt_irrefl _ H11). assert (H14 := Nzorn H13 H12); elim H14; clear H14; intros x0 H14; - exists (pos_Rl lg0 x0); unfold constant_D_eq, open_interval in |- *; + exists (pos_Rl lg0 x0); unfold constant_D_eq, open_interval; intros; assert (H16 := H4 x0); assert (H17 : (x0 < pred (Rlength lg))%nat). elim H14; clear H14; intros; unfold I in H14; elim H14; clear H14; intros; apply lt_S_n; replace (S (pred (Rlength lg))) with (Rlength lg). @@ -1454,12 +1452,12 @@ Proof. elim (RList_P6 (cons_ORlist lf lg)); intros; apply H21. apply RList_P2; assumption. apply lt_n_Sm_le; apply lt_n_S; assumption. - apply lt_pred_n_n; apply neq_O_lt; red in |- *; intro; rewrite <- H23 in H8; + apply lt_pred_n_n; apply neq_O_lt; red; intro; rewrite <- H23 in H8; elim (lt_n_O _ H8). right; rewrite H0; rewrite <- H5; apply RList_P16; try assumption. rewrite H0; assumption. rewrite <- H20; reflexivity. - apply S_pred with 0%nat; apply neq_O_lt; red in |- *; intro; + apply S_pred with 0%nat; apply neq_O_lt; red; intro; rewrite <- H19 in H18; elim (lt_n_O _ H18). assert (H18 := H16 H17); unfold constant_D_eq, open_interval in H18; rewrite (H18 x1). @@ -1471,11 +1469,11 @@ Proof. assert (H22 : (S x0 < Rlength lg)%nat). replace (Rlength lg) with (S (pred (Rlength lg))). apply lt_n_S; assumption. - symmetry in |- *; apply S_pred with 0%nat; apply neq_O_lt; red in |- *; + symmetry ; apply S_pred with 0%nat; apply neq_O_lt; red; intro; rewrite <- H22 in H21; elim (lt_n_O _ H21). elim (Rle_dec (pos_Rl lg (S x0)) (pos_Rl (cons_ORlist lf lg) i)); intro. assert (H23 : (S x0 <= x0)%nat); - [ apply H20; unfold I in |- *; split; assumption | elim (le_Sn_n _ H23) ]. + [ apply H20; unfold I; split; assumption | elim (le_Sn_n _ H23) ]. assert (H23 : pos_Rl (cons_ORlist lf lg) i < pos_Rl lg (S x0)). auto with real. clear b0; apply RList_P17; try assumption; @@ -1511,35 +1509,35 @@ Proof. intros i H8 x1 H10; unfold open_interval in H10, H9, H4; rewrite (H9 _ H8 _ H10); rewrite (H4 _ H8 _ H10); assert (H11 : l1 <> nil). - red in |- *; intro H11; rewrite H11 in H8; elim (lt_n_O _ H8). + red; intro H11; rewrite H11 in H8; elim (lt_n_O _ H8). destruct (RList_P19 _ H11) as (r,(r0,H12)); - rewrite H12; unfold FF in |- *; + rewrite H12; unfold FF; change (pos_Rl x0 i + l * pos_Rl x i = pos_Rl (app_Rlist (mid_Rlist (cons r r0) r) (fun x2:R => f x2 + l * g x2)) - (S i)) in |- *; rewrite RList_P12. + (S i)); rewrite RList_P12. rewrite RList_P13. rewrite <- H12; rewrite (H9 _ H8); try rewrite (H4 _ H8); reflexivity || (elim H10; clear H10; intros; split; [ apply Rmult_lt_reg_l with 2; [ prove_sup0 - | unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); + | unfold Rdiv; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym; [ rewrite Rmult_1_l; rewrite double; apply Rplus_lt_compat_l; apply Rlt_trans with x1; assumption | discrR ] ] | apply Rmult_lt_reg_l with 2; [ prove_sup0 - | unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); + | unfold Rdiv; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym; [ rewrite Rmult_1_l; rewrite double; rewrite (Rplus_comm (pos_Rl l1 i)); apply Rplus_lt_compat_l; apply Rlt_trans with x1; assumption | discrR ] ] ]). rewrite <- H12; assumption. - rewrite RList_P14; simpl in |- *; rewrite H12 in H8; simpl in H8; + rewrite RList_P14; simpl; rewrite H12 in H8; simpl in H8; apply lt_n_S; apply H8. Qed. @@ -1558,7 +1556,7 @@ Qed. Lemma StepFun_P28 : forall (a b l:R) (f g:StepFun a b), IsStepFun (fun x:R => f x + l * g x) a b. Proof. - intros a b l f g; unfold IsStepFun in |- *; assert (H := pre f); + intros a b l f g; unfold IsStepFun; assert (H := pre f); assert (H0 := pre g); unfold IsStepFun in H, H0; elim H; elim H0; intros; apply existT with (cons_ORlist x0 x); apply StepFun_P27; assumption. @@ -1567,7 +1565,7 @@ Qed. Lemma StepFun_P29 : forall (a b:R) (f:StepFun a b), is_subdivision f a b (subdivision f). Proof. - intros a b f; unfold is_subdivision in |- *; + intros a b f; unfold is_subdivision; apply existT with (subdivision_val f); apply StepFun_P1. Qed. @@ -1576,7 +1574,7 @@ Lemma StepFun_P30 : RiemannInt_SF (mkStepFun (StepFun_P28 l f g)) = RiemannInt_SF f + l * RiemannInt_SF g. Proof. - intros a b l f g; unfold RiemannInt_SF in |- *; case (Rle_dec a b); + intros a b l f g; unfold RiemannInt_SF; case (Rle_dec a b); (intro; replace (Int_SF (subdivision_val (mkStepFun (StepFun_P28 l f g))) @@ -1613,10 +1611,10 @@ Lemma StepFun_P31 : adapted_couple f a b l lf -> adapted_couple (fun x:R => Rabs (f x)) a b l (app_Rlist lf Rabs). Proof. - unfold adapted_couple in |- *; intros; decompose [and] H; clear H; + unfold adapted_couple; intros; decompose [and] H; clear H; repeat split; try assumption. - symmetry in |- *; rewrite H3; rewrite RList_P18; reflexivity. - intros; unfold constant_D_eq, open_interval in |- *; + symmetry ; rewrite H3; rewrite RList_P18; reflexivity. + intros; unfold constant_D_eq, open_interval; unfold constant_D_eq, open_interval in H5; intros; rewrite (H5 _ H _ H4); rewrite RList_P12; [ reflexivity | rewrite H3 in H; simpl in H; apply H ]. @@ -1625,8 +1623,8 @@ Qed. Lemma StepFun_P32 : forall (a b:R) (f:StepFun a b), IsStepFun (fun x:R => Rabs (f x)) a b. Proof. - intros a b f; unfold IsStepFun in |- *; apply existT with (subdivision f); - unfold is_subdivision in |- *; + intros a b f; unfold IsStepFun; apply existT with (subdivision f); + unfold is_subdivision; apply existT with (app_Rlist (subdivision_val f) Rabs); apply StepFun_P31; apply StepFun_P1. Qed. @@ -1636,8 +1634,8 @@ Lemma StepFun_P33 : ordered_Rlist l1 -> Rabs (Int_SF l2 l1) <= Int_SF (app_Rlist l2 Rabs) l1. Proof. simple induction l2; intros. - simpl in |- *; rewrite Rabs_R0; right; reflexivity. - simpl in |- *; induction l1 as [| r1 l1 Hrecl1]. + simpl; rewrite Rabs_R0; right; reflexivity. + simpl; induction l1 as [| r1 l1 Hrecl1]. rewrite Rabs_R0; right; reflexivity. induction l1 as [| r2 l1 Hrecl0]. rewrite Rabs_R0; right; reflexivity. @@ -1645,7 +1643,7 @@ Proof. apply Rabs_triang. rewrite Rabs_mult; rewrite (Rabs_right (r2 - r1)); [ apply Rplus_le_compat_l; apply H; apply RList_P4 with r1; assumption - | apply Rge_minus; apply Rle_ge; apply (H0 0%nat); simpl in |- *; + | apply Rge_minus; apply Rle_ge; apply (H0 0%nat); simpl; apply lt_O_Sn ]. Qed. @@ -1654,7 +1652,7 @@ Lemma StepFun_P34 : a <= b -> Rabs (RiemannInt_SF f) <= RiemannInt_SF (mkStepFun (StepFun_P32 f)). Proof. - intros; unfold RiemannInt_SF in |- *; case (Rle_dec a b); intro. + intros; unfold RiemannInt_SF; case (Rle_dec a b); intro. replace (Int_SF (subdivision_val (mkStepFun (StepFun_P32 f))) (subdivision (mkStepFun (StepFun_P32 f)))) with @@ -1678,18 +1676,18 @@ Lemma StepFun_P35 : Proof. simple induction l; intros. right; reflexivity. - simpl in |- *; induction r0 as [| r0 r1 Hrecr0]. + simpl; induction r0 as [| r0 r1 Hrecr0]. right; reflexivity. - simpl in |- *; apply Rplus_le_compat. + simpl; apply Rplus_le_compat. case (Req_dec r r0); intro. rewrite H4; right; ring. do 2 rewrite <- (Rmult_comm (r0 - r)); apply Rmult_le_compat_l. - apply Rge_le; apply Rge_minus; apply Rle_ge; apply (H0 0%nat); simpl in |- *; + apply Rge_le; apply Rge_minus; apply Rle_ge; apply (H0 0%nat); simpl; apply lt_O_Sn. apply H3; split. apply Rmult_lt_reg_l with 2. prove_sup0. - unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; + unfold Rdiv; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym. assert (H5 : r = a). apply H1. @@ -1702,7 +1700,7 @@ Proof. discrR. apply Rmult_lt_reg_l with 2. prove_sup0. - unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; + unfold Rdiv; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym. rewrite Rmult_1_l; rewrite double; assert (H5 : r0 <= b). replace b with @@ -1710,9 +1708,9 @@ Proof. replace r0 with (pos_Rl (cons r (cons r0 r1)) 1). elim (RList_P6 (cons r (cons r0 r1))); intros; apply H5. assumption. - simpl in |- *; apply le_n_S. + simpl; apply le_n_S. apply le_O_n. - simpl in |- *; apply lt_n_Sn. + simpl; apply lt_n_Sn. reflexivity. apply Rle_lt_trans with (r + b). apply Rplus_le_compat_l; assumption. @@ -1732,7 +1730,7 @@ Proof. intros; apply H3; elim H4; intros; split; try assumption. apply Rle_lt_trans with r0; try assumption. rewrite <- H1. - simpl in |- *; apply (H0 0%nat); simpl in |- *; apply lt_O_Sn. + simpl; apply (H0 0%nat); simpl; apply lt_O_Sn. Qed. Lemma StepFun_P36 : @@ -1743,16 +1741,16 @@ Lemma StepFun_P36 : (forall x:R, a < x < b -> f x <= g x) -> RiemannInt_SF f <= RiemannInt_SF g. Proof. - intros; unfold RiemannInt_SF in |- *; case (Rle_dec a b); intro. + intros; unfold RiemannInt_SF; case (Rle_dec a b); intro. replace (Int_SF (subdivision_val f) (subdivision f)) with (Int_SF (FF l f) l). replace (Int_SF (subdivision_val g) (subdivision g)) with (Int_SF (FF l g) l). unfold is_subdivision in X; elim X; clear X; intros; unfold adapted_couple in p; decompose [and] p; clear p; assert (H5 : Rmin a b = a); - [ unfold Rmin in |- *; case (Rle_dec a b); intro; + [ unfold Rmin; case (Rle_dec a b); intro; [ reflexivity | elim n; assumption ] | assert (H7 : Rmax a b = b); - [ unfold Rmax in |- *; case (Rle_dec a b); intro; + [ unfold Rmax; case (Rle_dec a b); intro; [ reflexivity | elim n; assumption ] | rewrite H5 in H3; rewrite H7 in H2; eapply StepFun_P35 with a b; assumption ] ]. @@ -1811,27 +1809,27 @@ Proof. assert (H7 : r1 <= b). rewrite <- H4; apply RList_P7; [ assumption | left; reflexivity ]. assert (H8 : IsStepFun g' a b). - unfold IsStepFun in |- *; assert (H8 := pre g); unfold IsStepFun in H8; + unfold IsStepFun; assert (H8 := pre g); unfold IsStepFun in H8; elim H8; intros lg H9; unfold is_subdivision in H9; elim H9; clear H9; intros lg2 H9; split with (cons a lg); - unfold is_subdivision in |- *; split with (cons (f a) lg2); + unfold is_subdivision; split with (cons (f a) lg2); unfold adapted_couple in H9; decompose [and] H9; clear H9; - unfold adapted_couple in |- *; repeat split. - unfold ordered_Rlist in |- *; intros; simpl in H9; + unfold adapted_couple; repeat split. + unfold ordered_Rlist; intros; simpl in H9; induction i as [| i Hreci]. - simpl in |- *; rewrite H12; replace (Rmin r1 b) with r1. - simpl in H0; rewrite <- H0; apply (H 0%nat); simpl in |- *; apply lt_O_Sn. - unfold Rmin in |- *; case (Rle_dec r1 b); intro; + simpl; rewrite H12; replace (Rmin r1 b) with r1. + simpl in H0; rewrite <- H0; apply (H 0%nat); simpl; apply lt_O_Sn. + unfold Rmin; case (Rle_dec r1 b); intro; [ reflexivity | elim n; assumption ]. apply (H10 i); apply lt_S_n. replace (S (pred (Rlength lg))) with (Rlength lg). apply H9. apply S_pred with 0%nat; apply neq_O_lt; intro; rewrite <- H14 in H9; elim (lt_n_O _ H9). - simpl in |- *; assert (H14 : a <= b). + simpl; assert (H14 : a <= b). rewrite <- H1; simpl in H0; rewrite <- H0; apply RList_P7; [ assumption | left; reflexivity ]. - unfold Rmin in |- *; case (Rle_dec a b); intro; + unfold Rmin; case (Rle_dec a b); intro; [ reflexivity | elim n; assumption ]. assert (H14 : a <= b). rewrite <- H1; simpl in H0; rewrite <- H0; apply RList_P7; @@ -1840,30 +1838,30 @@ Proof. rewrite <- H11; induction lg as [| r0 lg Hreclg]. simpl in H13; discriminate. reflexivity. - unfold Rmax in |- *; case (Rle_dec a b); case (Rle_dec r1 b); intros; + unfold Rmax; case (Rle_dec a b); case (Rle_dec r1 b); intros; reflexivity || elim n; assumption. - simpl in |- *; rewrite H13; reflexivity. + simpl; rewrite H13; reflexivity. intros; simpl in H9; induction i as [| i Hreci]. - unfold constant_D_eq, open_interval in |- *; simpl in |- *; intros; + unfold constant_D_eq, open_interval; simpl; intros; assert (H16 : Rmin r1 b = r1). - unfold Rmin in |- *; case (Rle_dec r1 b); intro; + unfold Rmin; case (Rle_dec r1 b); intro; [ reflexivity | elim n; assumption ]. rewrite H16 in H12; rewrite H12 in H14; elim H14; clear H14; intros _ H14; - unfold g' in |- *; case (Rle_dec r1 x); intro r3. + unfold g'; case (Rle_dec r1 x); intro r3. elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r3 H14)). reflexivity. change (constant_D_eq g' (open_interval (pos_Rl lg i) (pos_Rl lg (S i))) - (pos_Rl lg2 i)) in |- *; clear Hreci; assert (H16 := H15 i); + (pos_Rl lg2 i)); clear Hreci; assert (H16 := H15 i); assert (H17 : (i < pred (Rlength lg))%nat). apply lt_S_n. replace (S (pred (Rlength lg))) with (Rlength lg). assumption. - apply S_pred with 0%nat; apply neq_O_lt; red in |- *; intro; + apply S_pred with 0%nat; apply neq_O_lt; red; intro; rewrite <- H14 in H9; elim (lt_n_O _ H9). assert (H18 := H16 H17); unfold constant_D_eq, open_interval in H18; - unfold constant_D_eq, open_interval in |- *; intros; - assert (H19 := H18 _ H14); rewrite <- H19; unfold g' in |- *; + unfold constant_D_eq, open_interval; intros; + assert (H19 := H18 _ H14); rewrite <- H19; unfold g'; case (Rle_dec r1 x); intro. reflexivity. elim n; replace r1 with (Rmin r1 b). @@ -1874,17 +1872,17 @@ Proof. elim (RList_P3 lg (pos_Rl lg i)); intros; apply H21; exists i; split. reflexivity. apply lt_trans with (pred (Rlength lg)); try assumption. - apply lt_pred_n_n; apply neq_O_lt; red in |- *; intro; rewrite <- H22 in H17; + apply lt_pred_n_n; apply neq_O_lt; red; intro; rewrite <- H22 in H17; elim (lt_n_O _ H17). - unfold Rmin in |- *; case (Rle_dec r1 b); intro; + unfold Rmin; case (Rle_dec r1 b); intro; [ reflexivity | elim n0; assumption ]. exists (mkStepFun H8); split. - simpl in |- *; unfold g' in |- *; case (Rle_dec r1 b); intro. + simpl; unfold g'; case (Rle_dec r1 b); intro. assumption. elim n; assumption. intros; simpl in H9; induction i as [| i Hreci]. - unfold constant_D_eq, co_interval in |- *; simpl in |- *; intros; simpl in H0; - rewrite H0; elim H10; clear H10; intros; unfold g' in |- *; + unfold constant_D_eq, co_interval; simpl; intros; simpl in H0; + rewrite H0; elim H10; clear H10; intros; unfold g'; case (Rle_dec r1 x); intro r3. elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r3 H11)). reflexivity. @@ -1892,21 +1890,21 @@ Proof. change (constant_D_eq (mkStepFun H8) (co_interval (pos_Rl (cons r1 l) i) (pos_Rl (cons r1 l) (S i))) - (f (pos_Rl (cons r1 l) i))) in |- *; assert (H10 := H6 i); + (f (pos_Rl (cons r1 l) i))); assert (H10 := H6 i); assert (H11 : (i < pred (Rlength (cons r1 l)))%nat). - simpl in |- *; apply lt_S_n; assumption. + simpl; apply lt_S_n; assumption. assert (H12 := H10 H11); unfold constant_D_eq, co_interval in H12; - unfold constant_D_eq, co_interval in |- *; intros; - rewrite <- (H12 _ H13); simpl in |- *; unfold g' in |- *; + unfold constant_D_eq, co_interval; intros; + rewrite <- (H12 _ H13); simpl; unfold g'; case (Rle_dec r1 x); intro. reflexivity. elim n; elim H13; clear H13; intros; apply Rle_trans with (pos_Rl (cons r1 l) i); try assumption; - change (pos_Rl (cons r1 l) 0 <= pos_Rl (cons r1 l) i) in |- *; + change (pos_Rl (cons r1 l) 0 <= pos_Rl (cons r1 l) i); elim (RList_P6 (cons r1 l)); intros; apply H15; [ assumption | apply le_O_n - | simpl in |- *; apply lt_trans with (Rlength l); + | simpl; apply lt_trans with (Rlength l); [ apply lt_S_n; assumption | apply lt_n_Sn ] ]. Qed. @@ -1914,7 +1912,7 @@ Lemma StepFun_P39 : forall (a b:R) (f:StepFun a b), RiemannInt_SF f = - RiemannInt_SF (mkStepFun (StepFun_P6 (pre f))). Proof. - intros; unfold RiemannInt_SF in |- *; case (Rle_dec a b); case (Rle_dec b a); + intros; unfold RiemannInt_SF; case (Rle_dec a b); case (Rle_dec b a); intros. assert (H : adapted_couple f a b (subdivision f) (subdivision_val f)); [ apply StepFun_P1 @@ -1927,16 +1925,16 @@ Proof. | assert (H1 : a = b); [ apply Rle_antisym; assumption | rewrite (StepFun_P8 H H1); assert (H2 : b = a); - [ symmetry in |- *; apply H1 | rewrite (StepFun_P8 H0 H2); ring ] ] ] ]. + [ symmetry ; apply H1 | rewrite (StepFun_P8 H0 H2); ring ] ] ] ]. rewrite Ropp_involutive; eapply StepFun_P17; [ apply StepFun_P1 | apply StepFun_P2; set (H := StepFun_P6 (pre f)); unfold IsStepFun in H; - elim H; intros; unfold is_subdivision in |- *; + elim H; intros; unfold is_subdivision; elim p; intros; apply p0 ]. apply Ropp_eq_compat; eapply StepFun_P17; [ apply StepFun_P1 | apply StepFun_P2; set (H := StepFun_P6 (pre f)); unfold IsStepFun in H; - elim H; intros; unfold is_subdivision in |- *; + elim H; intros; unfold is_subdivision; elim p; intros; apply p0 ]. assert (H : a < b); [ auto with real @@ -1953,34 +1951,34 @@ Lemma StepFun_P40 : adapted_couple f a c (cons_Rlist l1 l2) (FF (cons_Rlist l1 l2) f). Proof. intros f a b c l1 l2 lf1 lf2 H H0 H1 H2; unfold adapted_couple in H1, H2; - unfold adapted_couple in |- *; decompose [and] H1; + unfold adapted_couple; decompose [and] H1; decompose [and] H2; clear H1 H2; repeat split. apply RList_P25; try assumption. - rewrite H10; rewrite H4; unfold Rmin, Rmax in |- *; case (Rle_dec a b); + rewrite H10; rewrite H4; unfold Rmin, Rmax; case (Rle_dec a b); case (Rle_dec b c); intros; (right; reflexivity) || (elim n; left; assumption). rewrite RList_P22. - rewrite H5; unfold Rmin, Rmax in |- *; case (Rle_dec a b); case (Rle_dec a c); + rewrite H5; unfold Rmin, Rmax; case (Rle_dec a b); case (Rle_dec a c); intros; [ reflexivity | elim n; apply Rle_trans with b; left; assumption | elim n; left; assumption | elim n0; left; assumption ]. - red in |- *; intro; rewrite H1 in H6; discriminate. + red; intro; rewrite H1 in H6; discriminate. rewrite RList_P24. - rewrite H9; unfold Rmin, Rmax in |- *; case (Rle_dec b c); case (Rle_dec a c); + rewrite H9; unfold Rmin, Rmax; case (Rle_dec b c); case (Rle_dec a c); intros; [ reflexivity | elim n; apply Rle_trans with b; left; assumption | elim n; left; assumption | elim n0; left; assumption ]. - red in |- *; intro; rewrite H1 in H11; discriminate. + red; intro; rewrite H1 in H11; discriminate. apply StepFun_P20. - rewrite RList_P23; apply neq_O_lt; red in |- *; intro. + rewrite RList_P23; apply neq_O_lt; red; intro. assert (H2 : (Rlength l1 + Rlength l2)%nat = 0%nat). - symmetry in |- *; apply H1. + symmetry ; apply H1. elim (plus_is_O _ _ H2); intros; rewrite H12 in H6; discriminate. - unfold constant_D_eq, open_interval in |- *; intros; + unfold constant_D_eq, open_interval; intros; elim (le_or_lt (S (S i)) (Rlength l1)); intro. assert (H14 : pos_Rl (cons_Rlist l1 l2) i = pos_Rl l1 i). apply RList_P26; apply lt_S_n; apply le_lt_n_Sm; apply le_S_n; @@ -1993,28 +1991,28 @@ Proof. elim (RList_P20 _ H16); intros r1 [r2 [r3 H17]]; rewrite H17; change (f x = pos_Rl (app_Rlist (mid_Rlist (cons_Rlist (cons r2 r3) l2) r1) f) i) - in |- *; rewrite RList_P12. + ; rewrite RList_P12. induction i as [| i Hreci]. - simpl in |- *; assert (H18 := H8 0%nat); + simpl; assert (H18 := H8 0%nat); unfold constant_D_eq, open_interval in H18; assert (H19 : (0 < pred (Rlength l1))%nat). - rewrite H17; simpl in |- *; apply lt_O_Sn. + rewrite H17; simpl; apply lt_O_Sn. assert (H20 := H18 H19); repeat rewrite H20. reflexivity. assert (H21 : r1 <= r2). rewrite H17 in H3; apply (H3 0%nat). - simpl in |- *; apply lt_O_Sn. + simpl; apply lt_O_Sn. elim H21; intro. split. - rewrite H17; simpl in |- *; apply Rmult_lt_reg_l with 2; + rewrite H17; simpl; apply Rmult_lt_reg_l with 2; [ prove_sup0 - | unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; + | unfold Rdiv; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym; [ rewrite Rmult_1_l; rewrite double; apply Rplus_lt_compat_l; assumption | discrR ] ]. - rewrite H17; simpl in |- *; apply Rmult_lt_reg_l with 2; + rewrite H17; simpl; apply Rmult_lt_reg_l with 2; [ prove_sup0 - | unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; + | unfold Rdiv; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym; [ rewrite Rmult_1_l; rewrite (Rplus_comm r1); rewrite double; apply Rplus_lt_compat_l; assumption @@ -2043,13 +2041,13 @@ Proof. split. apply Rmult_lt_reg_l with 2; [ prove_sup0 - | unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; + | unfold Rdiv; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym; [ rewrite Rmult_1_l; rewrite double; apply Rplus_lt_compat_l; assumption | discrR ] ]. apply Rmult_lt_reg_l with 2; [ prove_sup0 - | unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; + | unfold Rdiv; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym; [ rewrite Rmult_1_l; rewrite (Rplus_comm (pos_Rl l1 (S i))); rewrite double; apply Rplus_lt_compat_l; assumption @@ -2057,21 +2055,21 @@ Proof. elim H2; intros; rewrite H22 in H23; elim (Rlt_irrefl _ (Rlt_trans _ _ _ H23 H24)). assumption. - simpl in |- *; rewrite H17 in H1; simpl in H1; apply lt_S_n; assumption. + simpl; rewrite H17 in H1; simpl in H1; apply lt_S_n; assumption. rewrite RList_P14; rewrite H17 in H1; simpl in H1; apply H1. inversion H12. assert (H16 : pos_Rl (cons_Rlist l1 l2) (S i) = b). rewrite RList_P29. - rewrite H15; rewrite <- minus_n_n; rewrite H10; unfold Rmin in |- *; + rewrite H15; rewrite <- minus_n_n; rewrite H10; unfold Rmin; case (Rle_dec b c); intro; [ reflexivity | elim n; left; assumption ]. rewrite H15; apply le_n. induction l1 as [| r l1 Hrecl1]. simpl in H15; discriminate. - clear Hrecl1; simpl in H1; simpl in |- *; apply lt_n_S; assumption. + clear Hrecl1; simpl in H1; simpl; apply lt_n_S; assumption. assert (H17 : pos_Rl (cons_Rlist l1 l2) i = b). rewrite RList_P26. replace i with (pred (Rlength l1)); - [ rewrite H4; unfold Rmax in |- *; case (Rle_dec a b); intro; + [ rewrite H4; unfold Rmax; case (Rle_dec a b); intro; [ reflexivity | elim n; left; assumption ] | rewrite H15; reflexivity ]. rewrite H15; apply lt_n_Sn. @@ -2089,22 +2087,22 @@ Proof. apply le_S_n; apply le_trans with (S i); [ assumption | apply le_n_Sn ]. induction l1 as [| r l1 Hrecl1]. simpl in H6; discriminate. - clear Hrecl1; simpl in H1; simpl in |- *; apply lt_n_S; assumption. - symmetry in |- *; apply minus_Sn_m; apply le_S_n; assumption. + clear Hrecl1; simpl in H1; simpl; apply lt_n_S; assumption. + symmetry ; apply minus_Sn_m; apply le_S_n; assumption. assert (H18 : (2 <= Rlength l1)%nat). clear f c l2 lf2 H0 H3 H8 H7 H10 H9 H11 H13 i H1 x H2 H12 m H14 H15 H16 H17; induction l1 as [| r l1 Hrecl1]. discriminate. clear Hrecl1; induction l1 as [| r0 l1 Hrecl1]. simpl in H5; simpl in H4; assert (H0 : Rmin a b < Rmax a b). - unfold Rmin, Rmax in |- *; case (Rle_dec a b); intro; + unfold Rmin, Rmax; case (Rle_dec a b); intro; [ assumption | elim n; left; assumption ]. rewrite <- H5 in H0; rewrite <- H4 in H0; elim (Rlt_irrefl _ H0). - clear Hrecl1; simpl in |- *; repeat apply le_n_S; apply le_O_n. + clear Hrecl1; simpl; repeat apply le_n_S; apply le_O_n. elim (RList_P20 _ H18); intros r1 [r2 [r3 H19]]; rewrite H19; change (f x = pos_Rl (app_Rlist (mid_Rlist (cons_Rlist (cons r2 r3) l2) r1) f) i) - in |- *; rewrite RList_P12. + ; rewrite RList_P12. induction i as [| i Hreci]. assert (H20 := le_S_n _ _ H15); assert (H21 := le_trans _ _ _ H18 H20); elim (le_Sn_O _ H21). @@ -2122,7 +2120,7 @@ Proof. assert (H21 : (S i - Rlength l1 < pred (Rlength l2))%nat). apply lt_pred; rewrite minus_Sn_m. apply plus_lt_reg_l with (Rlength l1); rewrite <- le_plus_minus. - rewrite H19 in H1; simpl in H1; rewrite H19; simpl in |- *; + rewrite H19 in H1; simpl in H1; rewrite H19; simpl; rewrite RList_P23 in H1; apply lt_n_S; assumption. apply le_trans with (S i); [ apply le_S_n; assumption | apply le_n_Sn ]. apply le_S_n; assumption. @@ -2134,7 +2132,7 @@ Proof. apply H7; apply lt_pred. rewrite minus_Sn_m. apply plus_lt_reg_l with (Rlength l1); rewrite <- le_plus_minus. - rewrite H19 in H1; simpl in H1; rewrite H19; simpl in |- *; + rewrite H19 in H1; simpl in H1; rewrite H19; simpl; rewrite RList_P23 in H1; apply lt_n_S; assumption. apply le_trans with (S i); [ apply le_S_n; assumption | apply le_n_Sn ]. apply le_S_n; assumption. @@ -2142,13 +2140,13 @@ Proof. split. apply Rmult_lt_reg_l with 2; [ prove_sup0 - | unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; + | unfold Rdiv; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym; [ rewrite Rmult_1_l; rewrite double; apply Rplus_lt_compat_l; assumption | discrR ] ]. apply Rmult_lt_reg_l with 2; [ prove_sup0 - | unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; + | unfold Rdiv; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym; [ rewrite Rmult_1_l; rewrite (Rplus_comm (pos_Rl l2 (S i - Rlength l1))); rewrite double; apply Rplus_lt_compat_l; assumption @@ -2159,14 +2157,14 @@ Proof. rewrite H17 in H26; simpl in H24; rewrite H24 in H25; elim (Rlt_irrefl _ (Rlt_trans _ _ _ H25 H26)). assert (H23 : pos_Rl (cons_Rlist l1 l2) (S i) = pos_Rl l2 (S i - Rlength l1)). - rewrite H19; simpl in |- *; simpl in H16; apply H16. + rewrite H19; simpl; simpl in H16; apply H16. assert (H24 : pos_Rl (cons_Rlist l1 l2) (S (S i)) = pos_Rl l2 (S (S i - Rlength l1))). - rewrite H19; simpl in |- *; simpl in H17; apply H17. + rewrite H19; simpl; simpl in H17; apply H17. rewrite <- H23; rewrite <- H24; assumption. - simpl in |- *; rewrite H19 in H1; simpl in H1; apply lt_S_n; assumption. - rewrite RList_P14; rewrite H19 in H1; simpl in H1; simpl in |- *; apply H1. + simpl; rewrite H19 in H1; simpl in H1; apply lt_S_n; assumption. + rewrite RList_P14; rewrite H19 in H1; simpl in H1; simpl; apply H1. Qed. Lemma StepFun_P41 : @@ -2191,11 +2189,11 @@ Lemma StepFun_P42 : Int_SF (FF l1 f) l1 + Int_SF (FF l2 f) l2. Proof. intros l1 l2 f; induction l1 as [| r l1 IHl1]; intros H; - [ simpl in |- *; ring + [ simpl; ring | destruct l1 as [| r0 r1]; - [ simpl in H; simpl in |- *; destruct l2 as [| r0 r1]; - [ simpl in |- *; ring | simpl in |- *; simpl in H; rewrite H; ring ] - | simpl in |- *; rewrite Rplus_assoc; apply Rplus_eq_compat_l; apply IHl1; + [ simpl in H; simpl; destruct l2 as [| r0 r1]; + [ simpl; ring | simpl; simpl in H; rewrite H; ring ] + | simpl; rewrite Rplus_assoc; apply Rplus_eq_compat_l; apply IHl1; rewrite <- H; reflexivity ] ]. Qed. @@ -2231,27 +2229,27 @@ Proof. (Int_SF (FF (cons_Rlist l1 l2) f) (cons_Rlist l1 l2)). replace (Int_SF lf1 l1) with (Int_SF (FF l1 f) l1). replace (Int_SF lf2 l2) with (Int_SF (FF l2 f) l2). - symmetry in |- *; apply StepFun_P42. + symmetry ; apply StepFun_P42. unfold adapted_couple in H1, H2; decompose [and] H1; decompose [and] H2; - clear H1 H2; rewrite H11; rewrite H5; unfold Rmax, Rmin in |- *; + clear H1 H2; rewrite H11; rewrite H5; unfold Rmax, Rmin; case (Rle_dec a b); case (Rle_dec b c); intros; reflexivity || elim n; assumption. eapply StepFun_P17; - [ apply StepFun_P21; unfold is_subdivision in |- *; split with lf2; apply H2; + [ apply StepFun_P21; unfold is_subdivision; split with lf2; apply H2; assumption | assumption ]. eapply StepFun_P17; - [ apply StepFun_P21; unfold is_subdivision in |- *; split with lf1; apply H1 + [ apply StepFun_P21; unfold is_subdivision; split with lf1; apply H1 | assumption ]. eapply StepFun_P17; [ apply (StepFun_P40 H H0 H1 H2) | apply H3 ]. replace (Int_SF lf2 l2) with 0. rewrite Rplus_0_r; eapply StepFun_P17; [ apply H1 | rewrite <- H0 in H3; apply H3 ]. - symmetry in |- *; eapply StepFun_P8; [ apply H2 | assumption ]. + symmetry ; eapply StepFun_P8; [ apply H2 | assumption ]. replace (Int_SF lf1 l1) with 0. rewrite Rplus_0_l; eapply StepFun_P17; [ apply H2 | rewrite H in H3; apply H3 ]. - symmetry in |- *; eapply StepFun_P8; [ apply H1 | assumption ]. + symmetry ; eapply StepFun_P8; [ apply H1 | assumption ]. elim n; apply Rle_trans with b; assumption. apply Rplus_eq_reg_l with (Int_SF lf2 l2); replace (Int_SF lf2 l2 + (Int_SF lf1 l1 + - Int_SF lf2 l2)) with @@ -2266,24 +2264,24 @@ Proof. replace (Int_SF lf2 l2) with (Int_SF (FF l2 f) l2). apply StepFun_P42. unfold adapted_couple in H2, H3; decompose [and] H2; decompose [and] H3; - clear H3 H2; rewrite H10; rewrite H6; unfold Rmax, Rmin in |- *; + clear H3 H2; rewrite H10; rewrite H6; unfold Rmax, Rmin; case (Rle_dec a c); case (Rle_dec b c); intros; [ elim n; assumption | reflexivity | elim n0; assumption | elim n1; assumption ]. eapply StepFun_P17; - [ apply StepFun_P21; unfold is_subdivision in |- *; split with lf2; apply H2 + [ apply StepFun_P21; unfold is_subdivision; split with lf2; apply H2 | assumption ]. eapply StepFun_P17; - [ apply StepFun_P21; unfold is_subdivision in |- *; split with lf3; apply H3 + [ apply StepFun_P21; unfold is_subdivision; split with lf3; apply H3 | assumption ]. eapply StepFun_P17; [ apply (StepFun_P40 H0 H H3 (StepFun_P2 H2)) | apply H1 ]. replace (Int_SF lf3 l3) with 0. rewrite Rplus_0_r; eapply StepFun_P17; [ apply H1 | apply StepFun_P2; rewrite <- H0 in H2; apply H2 ]. - symmetry in |- *; eapply StepFun_P8; [ apply H3 | assumption ]. + symmetry ; eapply StepFun_P8; [ apply H3 | assumption ]. replace (Int_SF lf2 l2) with (Int_SF lf3 l3 + Int_SF lf1 l1). ring. elim r; intro. @@ -2291,19 +2289,19 @@ Proof. (Int_SF (FF (cons_Rlist l3 l1) f) (cons_Rlist l3 l1)). replace (Int_SF lf3 l3) with (Int_SF (FF l3 f) l3). replace (Int_SF lf1 l1) with (Int_SF (FF l1 f) l1). - symmetry in |- *; apply StepFun_P42. + symmetry ; apply StepFun_P42. unfold adapted_couple in H1, H3; decompose [and] H1; decompose [and] H3; - clear H3 H1; rewrite H9; rewrite H5; unfold Rmax, Rmin in |- *; + clear H3 H1; rewrite H9; rewrite H5; unfold Rmax, Rmin; case (Rle_dec a c); case (Rle_dec a b); intros; [ elim n; assumption | elim n1; assumption | reflexivity | elim n1; assumption ]. eapply StepFun_P17; - [ apply StepFun_P21; unfold is_subdivision in |- *; split with lf1; apply H1 + [ apply StepFun_P21; unfold is_subdivision; split with lf1; apply H1 | assumption ]. eapply StepFun_P17; - [ apply StepFun_P21; unfold is_subdivision in |- *; split with lf3; apply H3 + [ apply StepFun_P21; unfold is_subdivision; split with lf3; apply H3 | assumption ]. eapply StepFun_P17. assert (H0 : c < a). @@ -2313,7 +2311,7 @@ Proof. replace (Int_SF lf1 l1) with 0. rewrite Rplus_0_r; eapply StepFun_P17; [ apply H3 | rewrite <- H in H2; apply H2 ]. - symmetry in |- *; eapply StepFun_P8; [ apply H1 | assumption ]. + symmetry ; eapply StepFun_P8; [ apply H1 | assumption ]. assert (H : b < a). auto with real. replace (Int_SF lf2 l2) with (Int_SF lf3 l3 + Int_SF lf1 l1). @@ -2323,19 +2321,19 @@ Proof. (Int_SF (FF (cons_Rlist l1 l3) f) (cons_Rlist l1 l3)). replace (Int_SF lf3 l3) with (Int_SF (FF l3 f) l3). replace (Int_SF lf1 l1) with (Int_SF (FF l1 f) l1). - symmetry in |- *; apply StepFun_P42. + symmetry ; apply StepFun_P42. unfold adapted_couple in H1, H3; decompose [and] H1; decompose [and] H3; - clear H3 H1; rewrite H11; rewrite H5; unfold Rmax, Rmin in |- *; + clear H3 H1; rewrite H11; rewrite H5; unfold Rmax, Rmin; case (Rle_dec a c); case (Rle_dec a b); intros; [ elim n; assumption | reflexivity | elim n0; assumption | elim n1; assumption ]. eapply StepFun_P17; - [ apply StepFun_P21; unfold is_subdivision in |- *; split with lf1; apply H1 + [ apply StepFun_P21; unfold is_subdivision; split with lf1; apply H1 | assumption ]. eapply StepFun_P17; - [ apply StepFun_P21; unfold is_subdivision in |- *; split with lf3; apply H3 + [ apply StepFun_P21; unfold is_subdivision; split with lf3; apply H3 | assumption ]. eapply StepFun_P17. apply (StepFun_P40 H H0 (StepFun_P2 H1) H3). @@ -2343,7 +2341,7 @@ Proof. replace (Int_SF lf3 l3) with 0. rewrite Rplus_0_r; eapply StepFun_P17; [ apply H1 | rewrite <- H0 in H2; apply StepFun_P2; apply H2 ]. - symmetry in |- *; eapply StepFun_P8; [ apply H3 | assumption ]. + symmetry ; eapply StepFun_P8; [ apply H3 | assumption ]. assert (H : c < a). auto with real. replace (Int_SF lf1 l1) with (Int_SF lf2 l2 + Int_SF lf3 l3). @@ -2353,19 +2351,19 @@ Proof. (Int_SF (FF (cons_Rlist l2 l3) f) (cons_Rlist l2 l3)). replace (Int_SF lf3 l3) with (Int_SF (FF l3 f) l3). replace (Int_SF lf2 l2) with (Int_SF (FF l2 f) l2). - symmetry in |- *; apply StepFun_P42. + symmetry ; apply StepFun_P42. unfold adapted_couple in H2, H3; decompose [and] H2; decompose [and] H3; - clear H3 H2; rewrite H11; rewrite H5; unfold Rmax, Rmin in |- *; + clear H3 H2; rewrite H11; rewrite H5; unfold Rmax, Rmin; case (Rle_dec a c); case (Rle_dec b c); intros; [ elim n; assumption | elim n1; assumption | reflexivity | elim n1; assumption ]. eapply StepFun_P17; - [ apply StepFun_P21; unfold is_subdivision in |- *; split with lf2; apply H2 + [ apply StepFun_P21; unfold is_subdivision; split with lf2; apply H2 | assumption ]. eapply StepFun_P17; - [ apply StepFun_P21; unfold is_subdivision in |- *; split with lf3; apply H3 + [ apply StepFun_P21; unfold is_subdivision; split with lf3; apply H3 | assumption ]. eapply StepFun_P17. apply (StepFun_P40 H0 H H2 (StepFun_P2 H3)). @@ -2373,7 +2371,7 @@ Proof. replace (Int_SF lf2 l2) with 0. rewrite Rplus_0_l; eapply StepFun_P17; [ apply H3 | rewrite H0 in H1; apply H1 ]. - symmetry in |- *; eapply StepFun_P8; [ apply H2 | assumption ]. + symmetry ; eapply StepFun_P8; [ apply H2 | assumption ]. elim n; apply Rle_trans with a; try assumption. auto with real. assert (H : c < b). @@ -2386,56 +2384,56 @@ Proof. (Int_SF (FF (cons_Rlist l2 l1) f) (cons_Rlist l2 l1)). replace (Int_SF lf1 l1) with (Int_SF (FF l1 f) l1). replace (Int_SF lf2 l2) with (Int_SF (FF l2 f) l2). - symmetry in |- *; apply StepFun_P42. + symmetry ; apply StepFun_P42. unfold adapted_couple in H2, H1; decompose [and] H2; decompose [and] H1; - clear H1 H2; rewrite H11; rewrite H5; unfold Rmax, Rmin in |- *; + clear H1 H2; rewrite H11; rewrite H5; unfold Rmax, Rmin; case (Rle_dec a b); case (Rle_dec b c); intros; [ elim n1; assumption | elim n1; assumption | elim n0; assumption | reflexivity ]. eapply StepFun_P17; - [ apply StepFun_P21; unfold is_subdivision in |- *; split with lf2; apply H2 + [ apply StepFun_P21; unfold is_subdivision; split with lf2; apply H2 | assumption ]. eapply StepFun_P17; - [ apply StepFun_P21; unfold is_subdivision in |- *; split with lf1; apply H1 + [ apply StepFun_P21; unfold is_subdivision; split with lf1; apply H1 | assumption ]. eapply StepFun_P17. apply (StepFun_P40 H H0 (StepFun_P2 H2) (StepFun_P2 H1)). apply StepFun_P2; apply H3. - unfold RiemannInt_SF in |- *; case (Rle_dec a c); intro. + unfold RiemannInt_SF; case (Rle_dec a c); intro. eapply StepFun_P17. apply H3. change (adapted_couple (mkStepFun pr3) a c (subdivision (mkStepFun pr3)) - (subdivision_val (mkStepFun pr3))) in |- *; apply StepFun_P1. + (subdivision_val (mkStepFun pr3))); apply StepFun_P1. apply Ropp_eq_compat; eapply StepFun_P17. apply H3. change (adapted_couple (mkStepFun pr3) a c (subdivision (mkStepFun pr3)) - (subdivision_val (mkStepFun pr3))) in |- *; apply StepFun_P1. - unfold RiemannInt_SF in |- *; case (Rle_dec b c); intro. + (subdivision_val (mkStepFun pr3))); apply StepFun_P1. + unfold RiemannInt_SF; case (Rle_dec b c); intro. eapply StepFun_P17. apply H2. change (adapted_couple (mkStepFun pr2) b c (subdivision (mkStepFun pr2)) - (subdivision_val (mkStepFun pr2))) in |- *; apply StepFun_P1. + (subdivision_val (mkStepFun pr2))); apply StepFun_P1. apply Ropp_eq_compat; eapply StepFun_P17. apply H2. change (adapted_couple (mkStepFun pr2) b c (subdivision (mkStepFun pr2)) - (subdivision_val (mkStepFun pr2))) in |- *; apply StepFun_P1. - unfold RiemannInt_SF in |- *; case (Rle_dec a b); intro. + (subdivision_val (mkStepFun pr2))); apply StepFun_P1. + unfold RiemannInt_SF; case (Rle_dec a b); intro. eapply StepFun_P17. apply H1. change (adapted_couple (mkStepFun pr1) a b (subdivision (mkStepFun pr1)) - (subdivision_val (mkStepFun pr1))) in |- *; apply StepFun_P1. + (subdivision_val (mkStepFun pr1))); apply StepFun_P1. apply Ropp_eq_compat; eapply StepFun_P17. apply H1. change (adapted_couple (mkStepFun pr1) a b (subdivision (mkStepFun pr1)) - (subdivision_val (mkStepFun pr1))) in |- *; apply StepFun_P1. + (subdivision_val (mkStepFun pr1))); apply StepFun_P1. Qed. Lemma StepFun_P44 : @@ -2451,7 +2449,7 @@ Proof. adapted_couple f a b l1 lf1 -> a <= c <= b -> { l:Rlist & { l0:Rlist & adapted_couple f a c l l0 } }). - intro X; unfold IsStepFun in |- *; unfold is_subdivision in |- *; eapply X. + intro X; unfold IsStepFun; unfold is_subdivision; eapply X. apply H2. split; assumption. clear f a b c H0 H H1 H2 l1 lf1; simple induction l1. @@ -2463,11 +2461,11 @@ Proof. simpl in H2; assert (H7 : a <= b). elim H0; intros; apply Rle_trans with c; assumption. replace a with (Rmin a b). - pattern b at 2 in |- *; replace b with (Rmax a b). + pattern b at 2; replace b with (Rmax a b). rewrite <- H2; rewrite H3; reflexivity. - unfold Rmax in |- *; case (Rle_dec a b); intro; + unfold Rmax; case (Rle_dec a b); intro; [ reflexivity | elim n; assumption ]. - unfold Rmin in |- *; case (Rle_dec a b); intro; + unfold Rmin; case (Rle_dec a b); intro; [ reflexivity | elim n; assumption ]. split with (cons r nil); split with lf1; assert (H2 : c = b). rewrite H1 in H0; elim H0; intros; apply Rle_antisym; assumption. @@ -2481,22 +2479,22 @@ Proof. split with (cons r (cons c nil)); split with (cons r3 nil); unfold adapted_couple in H; decompose [and] H; clear H; assert (H6 : r = a). - simpl in H4; rewrite H4; unfold Rmin in |- *; case (Rle_dec a b); intro; + simpl in H4; rewrite H4; unfold Rmin; case (Rle_dec a b); intro; [ reflexivity | elim n; elim H0; intros; apply Rle_trans with c; assumption ]. - elim H0; clear H0; intros; unfold adapted_couple in |- *; repeat split. - rewrite H6; unfold ordered_Rlist in |- *; intros; simpl in H8; inversion H8; - [ simpl in |- *; assumption | elim (le_Sn_O _ H10) ]. - simpl in |- *; unfold Rmin in |- *; case (Rle_dec a c); intro; + elim H0; clear H0; intros; unfold adapted_couple; repeat split. + rewrite H6; unfold ordered_Rlist; intros; simpl in H8; inversion H8; + [ simpl; assumption | elim (le_Sn_O _ H10) ]. + simpl; unfold Rmin; case (Rle_dec a c); intro; [ assumption | elim n; assumption ]. - simpl in |- *; unfold Rmax in |- *; case (Rle_dec a c); intro; + simpl; unfold Rmax; case (Rle_dec a c); intro; [ reflexivity | elim n; assumption ]. - unfold constant_D_eq, open_interval in |- *; intros; simpl in H8; + unfold constant_D_eq, open_interval; intros; simpl in H8; inversion H8. - simpl in |- *; assert (H10 := H7 0%nat); + simpl; assert (H10 := H7 0%nat); assert (H12 : (0 < pred (Rlength (cons r (cons r1 r2))))%nat). - simpl in |- *; apply lt_O_Sn. - apply (H10 H12); unfold open_interval in |- *; simpl in |- *; + simpl; apply lt_O_Sn. + apply (H10 H12); unfold open_interval; simpl; rewrite H11 in H9; simpl in H9; elim H9; clear H9; intros; split; try assumption. apply Rlt_le_trans with c; assumption. @@ -2510,42 +2508,42 @@ Proof. assert (H14 : a <= b). elim H0; intros; apply Rle_trans with c; assumption. assert (H16 : r = a). - simpl in H7; rewrite H7; unfold Rmin in |- *; case (Rle_dec a b); intro; + simpl in H7; rewrite H7; unfold Rmin; case (Rle_dec a b); intro; [ reflexivity | elim n; assumption ]. induction l1' as [| r4 l1' Hrecl1']. simpl in H13; discriminate. - clear Hrecl1'; unfold adapted_couple in |- *; repeat split. - unfold ordered_Rlist in |- *; intros; simpl in H; induction i as [| i Hreci]. - simpl in |- *; replace r4 with r1. + clear Hrecl1'; unfold adapted_couple; repeat split. + unfold ordered_Rlist; intros; simpl in H; induction i as [| i Hreci]. + simpl; replace r4 with r1. apply (H5 0%nat). - simpl in |- *; apply lt_O_Sn. - simpl in H12; rewrite H12; unfold Rmin in |- *; case (Rle_dec r1 c); intro; + simpl; apply lt_O_Sn. + simpl in H12; rewrite H12; unfold Rmin; case (Rle_dec r1 c); intro; [ reflexivity | elim n; left; assumption ]. - apply (H9 i); simpl in |- *; apply lt_S_n; assumption. - simpl in |- *; unfold Rmin in |- *; case (Rle_dec a c); intro; + apply (H9 i); simpl; apply lt_S_n; assumption. + simpl; unfold Rmin; case (Rle_dec a c); intro; [ assumption | elim n; elim H0; intros; assumption ]. replace (Rmax a c) with (Rmax r1 c). rewrite <- H11; reflexivity. - unfold Rmax in |- *; case (Rle_dec r1 c); case (Rle_dec a c); intros; + unfold Rmax; case (Rle_dec r1 c); case (Rle_dec a c); intros; [ reflexivity | elim n; elim H0; intros; assumption | elim n; left; assumption | elim n0; left; assumption ]. - simpl in |- *; simpl in H13; rewrite H13; reflexivity. - intros; simpl in H; unfold constant_D_eq, open_interval in |- *; intros; + simpl; simpl in H13; rewrite H13; reflexivity. + intros; simpl in H; unfold constant_D_eq, open_interval; intros; induction i as [| i Hreci]. - simpl in |- *; assert (H17 := H10 0%nat); + simpl; assert (H17 := H10 0%nat); assert (H18 : (0 < pred (Rlength (cons r (cons r1 r2))))%nat). - simpl in |- *; apply lt_O_Sn. - apply (H17 H18); unfold open_interval in |- *; simpl in |- *; simpl in H4; + simpl; apply lt_O_Sn. + apply (H17 H18); unfold open_interval; simpl; simpl in H4; elim H4; clear H4; intros; split; try assumption; replace r1 with r4. assumption. - simpl in H12; rewrite H12; unfold Rmin in |- *; case (Rle_dec r1 c); intro; + simpl in H12; rewrite H12; unfold Rmin; case (Rle_dec r1 c); intro; [ reflexivity | elim n; left; assumption ]. - clear Hreci; simpl in |- *; apply H15. - simpl in |- *; apply lt_S_n; assumption. - unfold open_interval in |- *; apply H4. + clear Hreci; simpl; apply H15. + simpl; apply lt_S_n; assumption. + unfold open_interval; apply H4. split. left; assumption. elim H0; intros; assumption. @@ -2567,7 +2565,7 @@ Proof. adapted_couple f a b l1 lf1 -> a <= c <= b -> { l:Rlist & { l0:Rlist & adapted_couple f c b l l0 } }). - intro X; unfold IsStepFun in |- *; unfold is_subdivision in |- *; eapply X; + intro X; unfold IsStepFun; unfold is_subdivision; eapply X; [ apply H2 | split; assumption ]. clear f a b c H0 H H1 H2 l1 lf1; simple induction l1. intros; unfold adapted_couple in H; decompose [and] H; clear H; simpl in H4; @@ -2578,11 +2576,11 @@ Proof. simpl in H2; assert (H7 : a <= b). elim H0; intros; apply Rle_trans with c; assumption. replace a with (Rmin a b). - pattern b at 2 in |- *; replace b with (Rmax a b). + pattern b at 2; replace b with (Rmax a b). rewrite <- H2; rewrite H3; reflexivity. - unfold Rmax in |- *; case (Rle_dec a b); intro; + unfold Rmax; case (Rle_dec a b); intro; [ reflexivity | elim n; assumption ]. - unfold Rmin in |- *; case (Rle_dec a b); intro; + unfold Rmin; case (Rle_dec a b); intro; [ reflexivity | elim n; assumption ]. split with (cons r nil); split with lf1; assert (H2 : c = b). rewrite H1 in H0; elim H0; intros; apply Rle_antisym; assumption. @@ -2595,32 +2593,32 @@ Proof. elim H1; intro. split with (cons c (cons r1 r2)); split with (cons r3 lf1); unfold adapted_couple in H; decompose [and] H; clear H; - unfold adapted_couple in |- *; repeat split. - unfold ordered_Rlist in |- *; intros; simpl in H; induction i as [| i Hreci]. - simpl in |- *; assumption. - clear Hreci; apply (H2 (S i)); simpl in |- *; assumption. - simpl in |- *; unfold Rmin in |- *; case (Rle_dec c b); intro; + unfold adapted_couple; repeat split. + unfold ordered_Rlist; intros; simpl in H; induction i as [| i Hreci]. + simpl; assumption. + clear Hreci; apply (H2 (S i)); simpl; assumption. + simpl; unfold Rmin; case (Rle_dec c b); intro; [ reflexivity | elim n; elim H0; intros; assumption ]. replace (Rmax c b) with (Rmax a b). rewrite <- H3; reflexivity. - unfold Rmax in |- *; case (Rle_dec a b); case (Rle_dec c b); intros; + unfold Rmax; case (Rle_dec a b); case (Rle_dec c b); intros; [ reflexivity | elim n; elim H0; intros; assumption | elim n; elim H0; intros; apply Rle_trans with c; assumption | elim n0; elim H0; intros; apply Rle_trans with c; assumption ]. - simpl in |- *; simpl in H5; apply H5. + simpl; simpl in H5; apply H5. intros; simpl in H; induction i as [| i Hreci]. - unfold constant_D_eq, open_interval in |- *; intros; simpl in |- *; + unfold constant_D_eq, open_interval; intros; simpl; apply (H7 0%nat). - simpl in |- *; apply lt_O_Sn. - unfold open_interval in |- *; simpl in |- *; simpl in H6; elim H6; clear H6; + simpl; apply lt_O_Sn. + unfold open_interval; simpl; simpl in H6; elim H6; clear H6; intros; split; try assumption; apply Rle_lt_trans with c; try assumption; replace r with a. elim H0; intros; assumption. - simpl in H4; rewrite H4; unfold Rmin in |- *; case (Rle_dec a b); intros; + simpl in H4; rewrite H4; unfold Rmin; case (Rle_dec a b); intros; [ reflexivity | elim n; elim H0; intros; apply Rle_trans with c; assumption ]. - clear Hreci; apply (H7 (S i)); simpl in |- *; assumption. + clear Hreci; apply (H7 (S i)); simpl; assumption. cut (adapted_couple f r1 b (cons r1 r2) lf1). cut (r1 <= c <= b). intros; elim (X0 _ _ _ _ _ H3 H2); intros l1' [lf1' H4]; split with l1'; |