diff options
author | Samuel Mimram <smimram@debian.org> | 2006-01-19 22:34:29 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2006-01-19 22:34:29 +0000 |
commit | 018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (patch) | |
tree | fbb91e2f74c73bb867ab62c58f248a704bbe6dec /theories/Reals/PartSum.v | |
parent | 6497f27021fec4e01f2182014f2bb1989b4707f9 (diff) |
Imported Upstream version 8.0pl3upstream/8.0pl3
Diffstat (limited to 'theories/Reals/PartSum.v')
-rw-r--r-- | theories/Reals/PartSum.v | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/theories/Reals/PartSum.v b/theories/Reals/PartSum.v index 13070bde..6087d3f2 100644 --- a/theories/Reals/PartSum.v +++ b/theories/Reals/PartSum.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: PartSum.v,v 1.11.2.1 2004/07/16 19:31:11 herbelin Exp $ i*) +(*i $Id: PartSum.v,v 1.11.2.2 2005/07/13 22:28:30 herbelin Exp $ i*) Require Import Rbase. Require Import Rfunctions. @@ -489,8 +489,7 @@ elim s; intro. left; apply a. right; apply b. cut (Un_growing (fun n:nat => sum_f_R0 An n)). -intro; set (l1 := sum_f_R0 An N). -fold l1 in r. +intro; set (l1 := sum_f_R0 An N) in r. unfold Un_cv in H; cut (0 < l1 - l). intro; elim (H _ H2); intros. set (N0 := max x N); cut (N0 >= x)%nat. @@ -600,4 +599,4 @@ apply Rle_trans with (sum_f_R0 An n0 + Rabs (fn (S n0) x)). do 2 rewrite <- (Rplus_comm (Rabs (fn (S n0) x))). apply Rplus_le_compat_l; apply Hrecn0. apply Rplus_le_compat_l; apply H1. -Qed.
\ No newline at end of file +Qed. |