diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-07-13 22:29:44 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-07-13 22:29:44 +0000 |
| commit | e37c1b1114a37224d36531cee438561b04d798d0 (patch) | |
| tree | 33568a1e94db635222b0fe636577d61ea40d79cb /theories/Reals/PartSum.v | |
| parent | 04059dcd28255752042f97b0f0bc58872ed32631 (diff) | |
Détection d'un Fold incorrect suite à correction bug #986
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7219 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/PartSum.v')
| -rw-r--r-- | theories/Reals/PartSum.v | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/theories/Reals/PartSum.v b/theories/Reals/PartSum.v index d20b896a5..3e121ecf6 100644 --- a/theories/Reals/PartSum.v +++ b/theories/Reals/PartSum.v @@ -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. |