diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-12-24 10:27:08 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-12-24 10:27:08 +0000 |
| commit | 38734c5e122e9a38cf5b8afc586f47abced11361 (patch) | |
| tree | 2227afa958bf809d9152b526e29f183b552e5e61 /theories/Reals/PartSum.v | |
| parent | c69ae2a1f05db124c19b7f326ca23e980f643198 (diff) | |
changement de pose en set (pose n'etait pas utilise avec la semantique
documentee).
Reste a retablir la semantique de pose.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5141 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/PartSum.v')
| -rw-r--r-- | theories/Reals/PartSum.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/theories/Reals/PartSum.v b/theories/Reals/PartSum.v index c12aea9df..6a65ade8b 100644 --- a/theories/Reals/PartSum.v +++ b/theories/Reals/PartSum.v @@ -212,7 +212,7 @@ assumption. cut (0 < Rabs ((l1 - l2) / 2)); [ intro | apply Rabs_pos_lt ]. elim (H (Rabs ((l1 - l2) / 2)) H2); intros. elim (H0 (Rabs ((l1 - l2) / 2)) H2); intros. -pose (N := max x0 x); cut (N >= x0)%nat. +set (N := max x0 x); cut (N >= x0)%nat. cut (N >= x)%nat. intros; assert (H7 := H3 N H5); assert (H8 := H4 N H6). cut (Rabs (l1 - l2) <= R_dist (sum_f_R0 An N) l1 + R_dist (sum_f_R0 An N) l2). @@ -390,7 +390,7 @@ do 2 rewrite Rabs_Ropp. rewrite (Rabs_right (sum_f_R0 (fun i:nat => Rabs (An (S n + i)%nat)) (m - S n))) . -pose (Bn := fun i:nat => An (S n + i)%nat). +set (Bn := fun i:nat => An (S n + i)%nat). replace (fun i:nat => Rabs (An (S n + i)%nat)) with (fun i:nat => Rabs (Bn i)). apply Rabs_triang_gen. @@ -415,7 +415,7 @@ do 2 rewrite Rplus_0_r. rewrite (Rabs_right (sum_f_R0 (fun i:nat => Rabs (An (S m + i)%nat)) (n - S m))) . -pose (Bn := fun i:nat => An (S m + i)%nat). +set (Bn := fun i:nat => An (S m + i)%nat). replace (fun i:nat => Rabs (An (S m + i)%nat)) with (fun i:nat => Rabs (Bn i)). apply Rabs_triang_gen. @@ -489,11 +489,11 @@ elim s; intro. left; apply a. right; apply b. cut (Un_growing (fun n:nat => sum_f_R0 An n)). -intro; pose (l1 := sum_f_R0 An N). +intro; set (l1 := sum_f_R0 An N). fold l1 in r. unfold Un_cv in H; cut (0 < l1 - l). intro; elim (H _ H2); intros. -pose (N0 := max x N); cut (N0 >= x)%nat. +set (N0 := max x N); cut (N0 >= x)%nat. intro; assert (H5 := H3 N0 H4). cut (l1 <= sum_f_R0 An N0). intro; unfold R_dist in H5; rewrite Rabs_right in H5. @@ -534,7 +534,7 @@ intro; cut (0 < (Rabs l1 - l2) / 2). intro; unfold Un_cv in H, H0. elim (H _ H3); intros Na H4. elim (H0 _ H3); intros Nb H5. -pose (N := max Na Nb). +set (N := max Na Nb). unfold R_dist in H4, H5. cut (Rabs (sum_f_R0 An N - l2) < (Rabs l1 - l2) / 2). intro; cut (Rabs (Rabs l1 - Rabs (SP fn N x)) < (Rabs l1 - l2) / 2). |