Removed SeqProp's dependency on Classical.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12796 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 11 insertions, 5 deletions

diff --git a/theories/Reals/Rseries.v b/theories/Reals/Rseries.v
index 15f02c69b..1ed6b03c5 100644
--- a/theories/Reals/Rseries.v
+++ b/theories/Reals/Rseries.v
@@ -100,12 +100,9 @@ Section sequence.
   Qed.
 
 (*********)
-  Lemma Un_cv_crit : Un_growing -> bound EUn ->  exists l : R, Un_cv l.
+  Lemma Un_cv_crit_lub : Un_growing -> forall l, is_lub EUn l -> Un_cv l.
   Proof.
-    intros Hug Heub.
-    destruct (completeness EUn Heub EUn_noempty) as (l, H).
-    exists l.
-    intros eps Heps.
+    intros Hug l H eps Heps.
 
     cut (exists N, Un N > l - eps).
     intros (N, H3).
@@ -263,6 +260,15 @@ Section sequence.
   Qed.
 
 (*********)
+  Lemma Un_cv_crit : Un_growing -> bound EUn ->  exists l : R, Un_cv l.
+  Proof.
+    intros Hug Heub.
+    exists (projT1 (completeness EUn Heub EUn_noempty)).
+    destruct (completeness EUn Heub EUn_noempty) as (l, H).
+    now apply Un_cv_crit_lub.
+  Qed.
+
+(*********)
   Lemma finite_greater :
     forall N:nat,  exists M : R, (forall n:nat, (n <= N)%nat -> Un n <= M).
   Proof.