From eab34b814f1d06767fee07690e3ab6a56236ccde Mon Sep 17 00:00:00 2001
From: Vincent Semeria
Date: Tue, 6 Aug 2019 18:47:57 +0200
Subject: Prove the completeness of real numbers from logical axiom sig_not_dec

---
 theories/QArith/QArith_base.v            |  30 ++
 theories/Reals/ConstructiveCauchyReals.v | 634 ++++++++++++++++++++++---------
 theories/Reals/ConstructiveRIneq.v       | 190 ++-------
 theories/Reals/ConstructiveRcomplete.v   | 576 +++++++++++++++++++++-------
 theories/Reals/Raxioms.v                 |  30 +-
 theories/Reals/Rdefinitions.v            |  25 +-
 6 files changed, 982 insertions(+), 503 deletions(-)

diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v
index 21bea6c315..1401f06986 100644
--- a/theories/QArith/QArith_base.v
+++ b/theories/QArith/QArith_base.v
@@ -726,6 +726,21 @@ Proof.
   exact (Z_lt_le_dec (Qnum x * QDen y) (Qnum y * QDen x)).
 Defined.
 
+Lemma Qarchimedean : forall q : Q, { p : positive | Qlt q (Z.pos p # 1) }.
+Proof.
+  intros. destruct q as [a b]. unfold Qlt. simpl.
+  rewrite Zmult_1_r. destruct a.
+  - exists xH. reflexivity.
+  - exists (p+1)%positive. apply (Z.lt_le_trans _ (Z.pos (p+1))).
+    apply Z.lt_succ_diag_r. rewrite Pos2Z.inj_mul.
+    rewrite <- (Zmult_1_r (Z.pos (p+1))). apply Z.mul_le_mono_nonneg.
+    discriminate. rewrite Zmult_1_r. apply Z.le_refl. discriminate.
+    apply Z2Nat.inj_le. discriminate. apply Pos2Z.is_nonneg.
+    apply Nat.le_succ_l. apply Nat2Z.inj_lt.
+    rewrite Z2Nat.id. apply Pos2Z.is_pos. apply Pos2Z.is_nonneg.
+  - exists xH. reflexivity.
+Qed.
+
 (** Compatibility of operations with respect to order. *)
 
 Lemma Qopp_le_compat : forall p q, p<=q -> -q <= -p.
@@ -980,6 +995,21 @@ change (1/b < c).
 apply Qlt_shift_div_r; assumption.
 Qed.
 
+Lemma Qinv_lt_contravar : forall a b : Q,
+    Qlt 0 a -> Qlt 0 b -> (Qlt a b <-> Qlt (/b) (/a)).
+Proof.
+  intros. split.
+  - intro. rewrite <- Qmult_1_l. apply Qlt_shift_div_r. apply H0.
+    rewrite <- (Qmult_inv_r a). rewrite Qmult_comm.
+    apply Qmult_lt_l. apply Qinv_lt_0_compat.  apply H.
+    apply H1. intro abs. rewrite abs in H. apply (Qlt_irrefl 0 H).
+  - intro. rewrite <- (Qinv_involutive b). rewrite <- (Qmult_1_l (// b)).
+    apply Qlt_shift_div_l. apply Qinv_lt_0_compat. apply H0.
+    rewrite <- (Qmult_inv_r a). apply Qmult_lt_l. apply H.
+    apply H1. intro abs. rewrite abs in H. apply (Qlt_irrefl 0 H).
+Qed.
+
+
 (** * Rational to the n-th power *)
 
 Definition Qpower_positive : Q -> positive -> Q :=
diff --git a/theories/Reals/ConstructiveCauchyReals.v b/theories/Reals/ConstructiveCauchyReals.v
index 3ca9248600..5de3c69e29 100644
--- a/theories/Reals/ConstructiveCauchyReals.v
+++ b/theories/Reals/ConstructiveCauchyReals.v
@@ -24,95 +24,9 @@ Open Scope Q.
    Constructive real numbers should be considered abstractly,
    forgetting the fact that they are implemented as rational sequences.
    All useful lemmas of this file are exposed in ConstructiveRIneq.v,
-   under more abstract names, like Rlt_asym instead of CRealLt_asym. *)
+   under more abstract names, like Rlt_asym instead of CRealLt_asym.
 
 
-(* First some limit results about Q *)
-Lemma Qarchimedean : forall q : Q, { p : positive | Qlt q (Z.pos p # 1) }.
-Proof.
-  intros. destruct q. unfold Qlt. simpl.
-  rewrite Zmult_1_r. destruct Qnum.
-  - exists xH. reflexivity.
-  - exists (p+1)%positive. apply (Z.lt_le_trans _ (Z.pos (p+1))).
-    apply Z.lt_succ_diag_r. rewrite Pos2Z.inj_mul.
-    rewrite <- (Zmult_1_r (Z.pos (p+1))). apply Z.mul_le_mono_nonneg.
-    discriminate. rewrite Zmult_1_r. apply Z.le_refl. discriminate.
-    apply Z2Nat.inj_le. discriminate. apply Pos2Z.is_nonneg.
-    apply Nat.le_succ_l. apply Nat2Z.inj_lt.
-    rewrite Z2Nat.id. apply Pos2Z.is_pos. apply Pos2Z.is_nonneg.
-  - exists xH. reflexivity.
-Qed.
-
-Lemma Qinv_lt_contravar : forall a b : Q,
-    Qlt 0 a -> Qlt 0 b -> (Qlt a b <-> Qlt (/b) (/a)).
-Proof.
-  intros. split.
-  - intro. rewrite <- Qmult_1_l. apply Qlt_shift_div_r. apply H0.
-    rewrite <- (Qmult_inv_r a). rewrite Qmult_comm.
-    apply Qmult_lt_l. apply Qinv_lt_0_compat.  apply H.
-    apply H1. intro abs. rewrite abs in H. apply (Qlt_irrefl 0 H).
-  - intro. rewrite <- (Qinv_involutive b). rewrite <- (Qmult_1_l (// b)).
-    apply Qlt_shift_div_l. apply Qinv_lt_0_compat. apply H0.
-    rewrite <- (Qmult_inv_r a). apply Qmult_lt_l. apply H.
-    apply H1. intro abs. rewrite abs in H. apply (Qlt_irrefl 0 H).
-Qed.
-
-Lemma Qabs_separation : forall q : Q,
-    (forall k:positive, Qlt (Qabs q) (1 # k))
-    -> q == 0.
-Proof.
-  intros. destruct (Qle_lt_or_eq 0 (Qabs q)). apply Qabs_nonneg.
-  - exfalso. destruct (Qarchimedean (Qinv (Qabs q))) as [p maj].
-    specialize (H p). apply (Qlt_not_le (/ Qabs q) (Z.pos p # 1)).
-    apply maj. apply Qlt_le_weak.
-    setoid_replace (Z.pos p # 1) with (/(1#p)). 2: reflexivity.
-    rewrite <- Qinv_lt_contravar. apply H. apply H0.
-    reflexivity.
-  - destruct q. unfold Qeq in H0. simpl in H0.
-    rewrite Zmult_1_r in H0. replace Qnum with 0%Z. reflexivity.
-    destruct (Zabs_dec Qnum). rewrite e. rewrite H0. reflexivity.
-    rewrite e. rewrite <- H0. ring.
-Qed.
-
-Lemma Qle_limit : forall (a b : Q),
-    (forall eps:Q, Qlt 0 eps -> Qlt a (b + eps))
-    -> Qle a b.
-Proof.
-  intros. destruct (Q_dec a b). destruct s.
-  apply Qlt_le_weak. assumption. exfalso.
-  assert (0 < a - b). unfold Qminus. apply (Qlt_minus_iff b a).
-  assumption. specialize (H (a-b) H0).
-  apply (Qlt_irrefl a). ring_simplify in H. assumption.
-  rewrite q. apply Qle_refl.
-Qed.
-
-Lemma Qopp_lt_compat : forall p q, p<q -> -q < -p.
-Proof.
-  intros (a1,a2) (b1,b2); unfold Qlt; simpl.
-  rewrite !Z.mul_opp_l. omega.
-Qed.
-
-Lemma Qmult_minus_one : forall q : Q, inject_Z (-1) * q == - q.
-Proof.
-  intros. field.
-Qed.
-
-Lemma Qsub_comm : forall a b : Q, - a + b == b - a.
-Proof.
-  intros. unfold Qeq. simpl. rewrite Pos.mul_comm. ring.
-Qed.
-
-Lemma PosLt_le_total : forall p q, Pos.lt p q \/ Pos.le q p.
-Proof.
-  intros. destruct (Pos.lt_total p q). left. assumption.
-  right. destruct H. subst q. apply Pos.le_refl. unfold Pos.lt in H.
-  unfold Pos.le. rewrite H. discriminate.
-Qed.
-
-
-
-
-(*
    Cauchy reals are Cauchy sequences of rational numbers,
    equipped with explicit moduli of convergence and
    an equivalence relation (the difference converges to zero).
@@ -301,77 +215,6 @@ Bind Scope R_scope_constr with CReal.
 Open Scope R_scope_constr.
 
 
-
-
-(* The equality on Cauchy reals is just QSeqEquiv,
-   which is independant of the convergence modulus. *)
-Lemma CRealEq_modindep : forall (x y : CReal),
-    QSeqEquivEx (proj1_sig x) (proj1_sig y)
-    <-> forall n:positive, Qle (Qabs (proj1_sig x (Pos.to_nat n) - proj1_sig y (Pos.to_nat n)))
-                        (2 # n).
-Proof.
-  intros [xn limx] [yn limy]. unfold proj1_sig. split.
-  - intros [cvmod H] n. unfold proj1_sig in H.
-    apply Qle_limit. intros.
-    destruct (Qarchimedean (/eps)) as [k maj].
-    remember (max (cvmod k) (Pos.to_nat n)) as p.
-    assert (le (cvmod k) p).
-    { rewrite Heqp. apply Nat.le_max_l. }
-    assert (Pos.to_nat n <= p)%nat.
-    { rewrite Heqp. apply Nat.le_max_r. }
-    specialize (H k p p H1 H1).
-    setoid_replace (xn (Pos.to_nat n) - yn (Pos.to_nat n))
-      with (xn (Pos.to_nat n) - xn p + (xn p - yn p + (yn p - yn (Pos.to_nat n)))).
-    apply (Qle_lt_trans _ (Qabs (xn (Pos.to_nat n) - xn p)
-                           + Qabs (xn p - yn p + (yn p - yn (Pos.to_nat n))))).
-    apply Qabs_triangle.
-    setoid_replace (2 # n) with ((1 # n) + (1#n)). rewrite <- Qplus_assoc.
-    apply Qplus_lt_le_compat.
-    apply limx. apply le_refl. assumption.
-    apply (Qle_trans _ (Qabs (xn p - yn p) + Qabs (yn p - yn (Pos.to_nat n)))).
-    apply Qabs_triangle. rewrite (Qplus_comm (1#n)). apply Qplus_le_compat.
-    apply Qle_lteq. left. apply (Qlt_trans _ (1 # k)).
-    assumption.
-    setoid_replace (Z.pos k #1) with (/ (1#k)) in maj. 2: reflexivity.
-    apply Qinv_lt_contravar. reflexivity. apply H0. apply maj.
-    apply Qle_lteq. left.
-    apply limy. assumption. apply le_refl.
-    ring_simplify. reflexivity. field.
-  - intros. exists (fun q => Pos.to_nat (2 * (3 * q))). intros k p q H0 H1.
-    unfold proj1_sig. specialize (H (2 * (3 * k))%positive).
-    assert ((Pos.to_nat (3 * k) <= Pos.to_nat (2 * (3 * k)))%nat).
-    { generalize (3 * k)%positive. intros. rewrite Pos2Nat.inj_mul.
-      rewrite <- (mult_1_l (Pos.to_nat p0)). apply Nat.mul_le_mono_nonneg.
-      auto. unfold Pos.to_nat. simpl. auto.
-      apply (le_trans 0 1). auto. apply Pos2Nat.is_pos. rewrite mult_1_l.
-      apply le_refl. }
-    setoid_replace (xn p - yn q)
-      with (xn p - xn (Pos.to_nat (2 * (3 * k)))
-            + (xn (Pos.to_nat (2 * (3 * k))) - yn (Pos.to_nat (2 * (3 * k)))
-               + (yn (Pos.to_nat (2 * (3 * k))) - yn q))).
-    setoid_replace (1 # k) with ((1 # 3 * k) + ((1 # 3 * k) + (1 # 3 * k))).
-    apply (Qle_lt_trans
-             _ (Qabs (xn p - xn (Pos.to_nat (2 * (3 * k))))
-                + (Qabs (xn (Pos.to_nat (2 * (3 * k))) - yn (Pos.to_nat (2 * (3 * k)))
-                         + (yn (Pos.to_nat (2 * (3 * k))) - yn q))))).
-    apply Qabs_triangle. apply Qplus_lt_le_compat.
-    apply limx. apply (le_trans _ (Pos.to_nat (2 * (3 * k)))). assumption. assumption.
-    assumption.
-    apply (Qle_trans
-             _ (Qabs (xn (Pos.to_nat (2 * (3 * k))) - yn (Pos.to_nat (2 * (3 * k))))
-                + Qabs (yn (Pos.to_nat (2 * (3 * k))) - yn q))).
-    apply Qabs_triangle. apply Qplus_le_compat.
-    setoid_replace (1 # 3 * k) with (2 # 2 * (3 * k)). apply H.
-    rewrite (factorDenom _ _ 3). rewrite (factorDenom _ _ 2). rewrite (factorDenom _ _ 3).
-    rewrite Qmult_assoc. rewrite (Qmult_comm (1#2)).
-    rewrite <- Qmult_assoc. apply Qmult_comp. reflexivity.
-    unfold Qeq. reflexivity.
-    apply Qle_lteq. left. apply limy. assumption.
-    apply (le_trans _ (Pos.to_nat (2 * (3 * k)))). assumption. assumption.
-    rewrite (factorDenom _ _ 3). ring_simplify. reflexivity. field.
-Qed.
-
-
 (* So QSeqEquiv is the equivalence relation of this constructive pre-order *)
 Definition CRealLt (x y : CReal) : Prop
   := exists n : positive, Qlt (2 # n)
@@ -409,6 +252,30 @@ Proof.
                     (proj1_sig y (S n) - proj1_sig x (S n))); assumption.
 Qed.
 
+(* CRealLt is decided by the LPO in Type,
+   which is a non-constructive oracle. *)
+Lemma CRealLt_lpo_dec : forall x y : CReal,
+    (forall (P : nat -> Prop), (forall n, {P n} + {~P n})
+                    -> {n | ~P n} + {forall n, P n})
+    -> { CRealLt x y } + { ~CRealLt x y }.
+Proof.
+  intros x y lpo.
+  destruct (lpo (fun n:nat => Qle (proj1_sig y (S n) - proj1_sig x (S n))
+                             (2 # Pos.of_nat (S n)))).
+  - intro n. destruct (Qlt_le_dec (2 # Pos.of_nat (S n))
+                                  (proj1_sig y (S n) - proj1_sig x (S n))).
+    right. apply Qlt_not_le. exact q. left. exact q.
+  - left. destruct s as [n nmaj]. exists (Pos.of_nat (S n)).
+    rewrite Nat2Pos.id. apply Qnot_le_lt. exact nmaj. discriminate.
+  - right. intro abs. destruct abs as [n majn].
+    specialize (q (pred (Pos.to_nat n))).
+    replace (S (pred (Pos.to_nat n))) with (Pos.to_nat n) in q.
+    rewrite Pos2Nat.id in q.
+    pose proof (Qle_not_lt _ _ q). contradiction.
+    symmetry. apply Nat.succ_pred. intro abs.
+    pose proof (Pos2Nat.is_pos n). rewrite abs in H. inversion H.
+Qed.
+
 (* Alias the quotient order equality *)
 Definition CRealEq (x y : CReal) : Prop
   := ~CRealLt x y /\ ~CRealLt y x.
@@ -465,6 +332,79 @@ Proof.
     apply Qle_Qabs. apply H.
 Qed.
 
+(* The equality on Cauchy reals is just QSeqEquiv,
+   which is independant of the convergence modulus. *)
+Lemma CRealEq_modindep : forall (x y : CReal),
+    QSeqEquivEx (proj1_sig x) (proj1_sig y)
+    <-> forall n:positive,
+      Qle (Qabs (proj1_sig x (Pos.to_nat n) - proj1_sig y (Pos.to_nat n))) (2 # n).
+Proof.
+  assert (forall x y: CReal, QSeqEquivEx (proj1_sig x) (proj1_sig y) -> x <= y ).
+  { intros [xn limx] [yn limy] [cvmod H] [n abs]. simpl in abs, H.
+    pose (xn (Pos.to_nat n) - yn (Pos.to_nat n) - (2#n)) as eps.
+    destruct (Qarchimedean (/eps)) as [k maj].
+    remember (max (cvmod k) (Pos.to_nat n)) as p.
+    assert (le (cvmod k) p).
+    { rewrite Heqp. apply Nat.le_max_l. }
+    assert (Pos.to_nat n <= p)%nat.
+    { rewrite Heqp. apply Nat.le_max_r. }
+    specialize (H k p p H0 H0).
+    setoid_replace (Z.pos k #1)%Q with (/ (1#k)) in maj. 2: reflexivity.
+    apply Qinv_lt_contravar in maj. 2: reflexivity. unfold eps in maj.
+    clear abs. (* less precise majoration *)
+    apply (Qplus_lt_r _ _ (2#n)) in maj. ring_simplify in maj.
+    apply (Qlt_not_le _ _ maj). clear maj.
+    setoid_replace (xn (Pos.to_nat n) + -1 * yn (Pos.to_nat n))
+      with (xn (Pos.to_nat n) - xn p + (xn p - yn p + (yn p - yn (Pos.to_nat n)))).
+    2: ring.
+    setoid_replace (2 # n)%Q with ((1 # n) + (1#n)).
+    rewrite <- Qplus_assoc.
+    apply Qplus_le_compat. apply (Qle_trans _ _ _ (Qle_Qabs _)).
+    apply Qlt_le_weak. apply limx. apply le_refl. assumption.
+    rewrite (Qplus_comm (1#n)).
+    apply Qplus_le_compat. apply (Qle_trans _ _ _ (Qle_Qabs _)).
+    apply Qlt_le_weak. exact H.
+    apply (Qle_trans _ _ _ (Qle_Qabs _)). apply Qlt_le_weak. apply limy.
+    assumption. apply le_refl. ring_simplify. reflexivity.
+    unfold eps. unfold Qminus. rewrite <- Qlt_minus_iff. exact abs. }
+  split.
+  - rewrite <- CRealEq_diff. intros. split.
+    apply H, QSeqEquivEx_sym. exact H0. apply H. exact H0.
+  - clear H. intros. destruct x as [xn limx], y as [yn limy].
+    exists (fun q => Pos.to_nat (2 * (3 * q))). intros k p q H0 H1.
+    unfold proj1_sig. specialize (H (2 * (3 * k))%positive).
+    assert ((Pos.to_nat (3 * k) <= Pos.to_nat (2 * (3 * k)))%nat).
+    { generalize (3 * k)%positive. intros. rewrite Pos2Nat.inj_mul.
+      rewrite <- (mult_1_l (Pos.to_nat p0)). apply Nat.mul_le_mono_nonneg.
+      auto. unfold Pos.to_nat. simpl. auto.
+      apply (le_trans 0 1). auto. apply Pos2Nat.is_pos. rewrite mult_1_l.
+      apply le_refl. }
+    setoid_replace (xn p - yn q)
+      with (xn p - xn (Pos.to_nat (2 * (3 * k)))
+            + (xn (Pos.to_nat (2 * (3 * k))) - yn (Pos.to_nat (2 * (3 * k)))
+               + (yn (Pos.to_nat (2 * (3 * k))) - yn q))).
+    setoid_replace (1 # k)%Q with ((1 # 3 * k) + ((1 # 3 * k) + (1 # 3 * k))).
+    apply (Qle_lt_trans
+             _ (Qabs (xn p - xn (Pos.to_nat (2 * (3 * k))))
+                + (Qabs (xn (Pos.to_nat (2 * (3 * k))) - yn (Pos.to_nat (2 * (3 * k)))
+                         + (yn (Pos.to_nat (2 * (3 * k))) - yn q))))).
+    apply Qabs_triangle. apply Qplus_lt_le_compat.
+    apply limx. apply (le_trans _ (Pos.to_nat (2 * (3 * k)))). assumption. assumption.
+    assumption.
+    apply (Qle_trans
+             _ (Qabs (xn (Pos.to_nat (2 * (3 * k))) - yn (Pos.to_nat (2 * (3 * k))))
+                + Qabs (yn (Pos.to_nat (2 * (3 * k))) - yn q))).
+    apply Qabs_triangle. apply Qplus_le_compat.
+    setoid_replace (1 # 3 * k)%Q with (2 # 2 * (3 * k))%Q. apply H.
+    rewrite (factorDenom _ _ 3). rewrite (factorDenom _ _ 2). rewrite (factorDenom _ _ 3).
+    rewrite Qmult_assoc. rewrite (Qmult_comm (1#2)).
+    rewrite <- Qmult_assoc. apply Qmult_comp. reflexivity.
+    unfold Qeq. reflexivity.
+    apply Qle_lteq. left. apply limy. assumption.
+    apply (le_trans _ (Pos.to_nat (2 * (3 * k)))). assumption. assumption.
+    rewrite (factorDenom _ _ 3). ring_simplify. reflexivity. field.
+Qed.
+
 (* Extend separation to all indices above *)
 Lemma CRealLt_aboveSig : forall (x y : CReal) (n : positive),
     (Qlt (2 # n)
@@ -565,17 +505,12 @@ Proof.
   intros x y H [n q].
   apply CRealLt_above in H. destruct H as [p H].
   pose proof (CRealLt_above_same y x n q).
-  destruct (PosLt_le_total n p).
-  - apply (Qlt_not_le (proj1_sig y (Pos.to_nat p)) (proj1_sig x (Pos.to_nat p))).
-    apply H0. unfold Pos.le. unfold Pos.lt in H1. rewrite H1. discriminate.
-    apply Qlt_le_weak. apply (Qplus_lt_l _ _ (-proj1_sig x (Pos.to_nat p))).
-    rewrite Qplus_opp_r. apply (Qlt_trans _ (2#p)).
-    unfold Qlt. simpl. unfold Z.lt. auto. apply H. apply Pos.le_refl.
-  - apply (Qlt_not_le (proj1_sig y (Pos.to_nat n)) (proj1_sig x (Pos.to_nat n))).
-    apply H0. apply Pos.le_refl. apply Qlt_le_weak.
-    apply (Qplus_lt_l _ _ (-proj1_sig x (Pos.to_nat n))).
-    rewrite Qplus_opp_r. apply (Qlt_trans _ (2#p)).
-    unfold Qlt. simpl. unfold Z.lt. auto. apply H. assumption.
+  apply (Qlt_not_le (proj1_sig y (Pos.to_nat (Pos.max n p)))
+                    (proj1_sig x (Pos.to_nat (Pos.max n p)))).
+  apply H0. apply Pos.le_max_l.
+  apply Qlt_le_weak. apply (Qplus_lt_l _ _ (-proj1_sig x (Pos.to_nat (Pos.max n p)))).
+  rewrite Qplus_opp_r. apply (Qlt_trans _ (2#p)).
+  unfold Qlt. simpl. unfold Z.lt. auto. apply H. apply Pos.le_max_r.
 Qed.
 
 Lemma CRealLt_irrefl : forall x:CReal, ~(x < x).
@@ -656,9 +591,10 @@ Proof.
     rewrite <- Qplus_assoc. rewrite <- Qplus_0_l.
     rewrite <- (Qplus_opp_r (1#n)). rewrite (Qplus_comm (1#n)).
     rewrite <- Qplus_assoc. apply Qplus_lt_le_compat.
-    + apply (Qplus_lt_l _ _ (1#n)). rewrite Qplus_opp_r.
-      apply (Qplus_lt_r _ _ (yn (Pos.to_nat n) - yn (Pos.to_nat (Pos.max n (4 * k))))).
-      ring_simplify. rewrite Qmult_minus_one.
+    + apply (Qplus_lt_r _ _ (yn (Pos.to_nat n) - yn (Pos.to_nat (Pos.max n (4 * k))) + (1#n)))
+      ; ring_simplify.
+      setoid_replace (-1 * yn (Pos.to_nat (Pos.max n (4 * k))))
+        with (- yn (Pos.to_nat (Pos.max n (4 * k)))). 2: ring.
       apply (Qle_lt_trans _ (Qabs (yn (Pos.to_nat n)
                                    - yn (Pos.to_nat (Pos.max n (4 * k)))))).
       apply Qle_Qabs. apply limy. apply le_refl. apply H.
@@ -692,13 +628,19 @@ Proof.
 Qed.
 
 Lemma CRealLt_Le_trans : forall x y z : CReal,
-    CRealLt x y
-    -> CRealLe y z -> CRealLt x z.
+    x < y -> y <= z -> x < z.
 Proof.
   intros.
   destruct (linear_order_T x z y H). apply c. contradiction.
 Qed.
 
+Lemma CRealLe_trans : forall x y z : CReal,
+    x <= y -> y <= z -> x <= z.
+Proof.
+  intros. intro abs. apply H0.
+  apply (CRealLt_Le_trans _ x); assumption.
+Qed.
+
 Lemma CRealLt_trans : forall x y z : CReal,
     x < y -> y < z -> x < z.
 Proof.
@@ -981,7 +923,7 @@ Proof.
   destruct x as [xn limx].
   exists (fun n : nat => - xn n).
   intros k p q H H0. unfold Qminus. rewrite Qopp_involutive.
-  rewrite Qsub_comm. apply limx; assumption.
+  rewrite Qplus_comm. apply limx; assumption.
 Defined.
 
 Notation "- x" := (CReal_opp x) : R_scope_constr.
@@ -1060,6 +1002,12 @@ Proof.
     apply H.
 Qed.
 
+Lemma CReal_plus_0_r : forall r : CReal,
+    r + 0 == r.
+Proof.
+  intro r. rewrite CReal_plus_comm. apply CReal_plus_0_l.
+Qed.
+
 Lemma CReal_plus_lt_compat_l :
   forall x y z : CReal,
     CRealLt y z
@@ -1080,9 +1028,7 @@ Proof.
 Qed.
 
 Lemma CReal_plus_lt_reg_l :
-  forall x y z : CReal,
-    CRealLt (CReal_plus x y) (CReal_plus x z)
-    -> CRealLt y z.
+  forall x y z : CReal, x + y < x + z -> y < z.
 Proof.
   intros. destruct H as [n maj]. exists (2*n)%positive.
   setoid_replace (proj1_sig z (Pos.to_nat (2 * n)) - proj1_sig y (Pos.to_nat (2 * n)))%Q
@@ -1095,6 +1041,27 @@ Proof.
   simpl; ring.
 Qed.
 
+Lemma CReal_plus_lt_reg_r :
+  forall x y z : CReal, y + x < z + x -> y < z.
+Proof.
+  intros x y z H. rewrite (CReal_plus_comm y), (CReal_plus_comm z) in H.
+  apply CReal_plus_lt_reg_l in H. exact H.
+Qed.
+
+Lemma CReal_plus_le_compat_l : forall r r1 r2, r1 <= r2 -> r + r1 <= r + r2.
+Proof.
+  intros. intro abs. apply CReal_plus_lt_reg_l in abs. contradiction.
+Qed.
+
+Lemma CReal_plus_le_lt_compat :
+  forall r1 r2 r3 r4 : CReal, r1 <= r2 -> r3 < r4 -> r1 + r3 < r2 + r4.
+Proof.
+  intros; apply CRealLe_Lt_trans with (r2 + r3).
+  intro abs. rewrite CReal_plus_comm, (CReal_plus_comm r1) in abs.
+  apply CReal_plus_lt_reg_l in abs. contradiction.
+  apply CReal_plus_lt_compat_l; exact H0.
+Qed.
+
 Lemma CReal_plus_opp_r : forall x : CReal,
     x + - x == 0.
 Proof.
@@ -1105,6 +1072,12 @@ Proof.
   unfold Qle. simpl. unfold Z.le. intro absurd. inversion absurd. field.
 Qed.
 
+Lemma CReal_plus_opp_l : forall x : CReal,
+    - x + x == 0.
+Proof.
+  intro x. rewrite CReal_plus_comm. apply CReal_plus_opp_r.
+Qed.
+
 Lemma CReal_plus_proper_r : forall x y z : CReal,
     CRealEq x y -> CRealEq (CReal_plus x z) (CReal_plus y z).
 Proof.
@@ -1144,7 +1117,7 @@ Proof.
   - intro abs. apply (CReal_plus_lt_compat_l r) in abs. contradiction.
 Qed.
 
-Fixpoint BoundFromZero (qn : nat -> Q) (k : nat) (A : positive) {struct k}
+Fixpoint BoundFromZero (qn : nat -> Q) (k : nat) (A : positive) { struct k }
   : (forall n:nat, le k n -> Qlt (Qabs (qn n)) (Z.pos A # 1))
     -> { B : positive | forall n:nat, Qlt (Qabs (qn n)) (Z.pos B # 1) }.
 Proof.
@@ -1492,8 +1465,7 @@ Proof.
 Qed.
 
 Lemma CReal_mult_plus_distr_l : forall r1 r2 r3 : CReal,
-    CRealEq (CReal_mult r1 (CReal_plus r2 r3))
-            (CReal_plus (CReal_mult r1 r2) (CReal_mult r1 r3)).
+    r1 * (r2 + r3) == (r1 * r2) + (r1 * r3).
 Proof.
   intros x y z. apply CRealEq_diff. apply CRealEq_modindep.
   apply (QSeqEquivEx_trans _ (fun n => proj1_sig x n
@@ -1613,6 +1585,15 @@ Proof.
     + rewrite Qinv_plus_distr. unfold Qeq. reflexivity.
 Qed.
 
+Lemma CReal_mult_plus_distr_r : forall r1 r2 r3 : CReal,
+    (r2 + r3) * r1 == (r2 * r1) + (r3 * r1).
+Proof.
+  intros.
+  rewrite CReal_mult_comm, CReal_mult_plus_distr_l,
+  <- (CReal_mult_comm r1), <- (CReal_mult_comm r1).
+  reflexivity.
+Qed.
+
 Lemma CReal_mult_1_l : forall r: CReal, 1 * r == r.
 Proof.
   intros [rn limr]. split.
@@ -1708,12 +1689,41 @@ Qed.
 
 Add Ring CRealRing : CReal_isRing.
 
+Lemma CReal_opp_0 : -0 == 0.
+Proof.
+  ring.
+Qed.
+
+Lemma CReal_opp_plus_distr : forall r1 r2, - (r1 + r2) == - r1 + - r2.
+Proof.
+  intros; ring.
+Qed.
+
+Lemma CReal_opp_involutive : forall x:CReal, --x == x.
+Proof.
+  intro x. ring.
+Qed.
+
+Lemma CReal_opp_gt_lt_contravar : forall r1 r2, r1 > r2 -> - r1 < - r2.
+Proof.
+  unfold CRealGt; intros.
+  apply (CReal_plus_lt_reg_l (r2 + r1)).
+  setoid_replace (r2 + r1 + - r1) with r2 by ring.
+  setoid_replace (r2 + r1 + - r2) with r1 by ring.
+  exact H.
+Qed.
+
 (**********)
 Lemma CReal_mult_0_l : forall r, 0 * r == 0.
 Proof.
   intro; ring.
 Qed.
 
+Lemma CReal_mult_0_r : forall r, r * 0 == 0.
+Proof.
+  intro; ring.
+Qed.
+
 (**********)
 Lemma CReal_mult_1_r : forall r, r * 1 == r.
 Proof.
@@ -1728,9 +1738,7 @@ Proof.
 Qed.
 
 Lemma CReal_mult_lt_compat_l : forall x y z : CReal,
-    CRealLt (inject_Q 0) x
-    -> CRealLt y z
-    -> CRealLt (CReal_mult x y) (CReal_mult x z).
+    0 < x -> y < z -> x*y < x*z.
 Proof.
   intros. apply (CReal_plus_lt_reg_l
                    (CReal_opp (CReal_mult x y))).
@@ -1744,6 +1752,13 @@ Proof.
   rewrite <- CReal_plus_assoc, H1, CReal_plus_0_l. exact H0.
 Qed.
 
+Lemma CReal_mult_lt_compat_r : forall x y z : CReal,
+    0 < x -> y < z -> y*x < z*x.
+Proof.
+  intros. rewrite <- (CReal_mult_comm x), <- (CReal_mult_comm x).
+  apply (CReal_mult_lt_compat_l x); assumption.
+Qed.
+
 Lemma CReal_mult_eq_reg_l : forall (r r1 r2 : CReal),
     r # 0
     -> CRealEq (CReal_mult r r1) (CReal_mult r r2)
@@ -1891,6 +1906,12 @@ Proof.
   intro p. rewrite <- INR_IPR. apply (lt_INR 0), Pos2Nat.is_pos.
 Qed.
 
+Lemma IPR_double : forall p:positive, IPR (2*p) == 2 * IPR p.
+Proof.
+  intro p. destruct p; try reflexivity.
+  rewrite CReal_mult_1_r. reflexivity.
+Qed.
+
 (**********)
 Lemma INR_IZR_INZ : forall n:nat, INR n == IZR (Z.of_nat n).
 Proof.
@@ -1939,6 +1960,77 @@ Proof.
     ring.
 Qed.
 
+Lemma mult_IPR : forall n m:positive, IPR (n * m) == IPR n * IPR m.
+Proof.
+  intros. repeat rewrite <- INR_IPR.
+  rewrite Pos2Nat.inj_mul. apply mult_INR.
+Qed.
+
+Lemma mult_IZR : forall n m:Z, IZR (n * m) == IZR n * IZR m.
+Proof.
+  intros n m. destruct n.
+  - rewrite CReal_mult_0_l. rewrite Z.mul_0_l. reflexivity.
+  - destruct m. rewrite Z.mul_0_r, CReal_mult_0_r. reflexivity.
+    simpl; unfold IZR. apply mult_IPR.
+    simpl. unfold IZR. rewrite mult_IPR. ring.
+  - destruct m. rewrite Z.mul_0_r, CReal_mult_0_r. reflexivity.
+    simpl. unfold IZR. rewrite mult_IPR. ring.
+    simpl. unfold IZR. rewrite mult_IPR. ring.
+Qed.
+
+Lemma opp_IZR : forall n:Z, IZR (- n) == - IZR n.
+Proof.
+  intros [|z|z]; unfold IZR. rewrite CReal_opp_0. reflexivity.
+  reflexivity. rewrite CReal_opp_involutive. reflexivity.
+Qed.
+
+Lemma minus_IZR : forall n m:Z, IZR (n - m) == IZR n - IZR m.
+Proof.
+  intros; unfold Z.sub, CReal_minus.
+  rewrite <- opp_IZR.
+  apply plus_IZR.
+Qed.
+
+Lemma IZR_lt : forall n m:Z, (n < m)%Z -> IZR n < IZR m.
+Proof.
+ assert (forall n:Z, Z.lt 0 n -> 0 < IZR n) as posCase.
+ { intros. destruct (IZN n). apply Z.lt_le_incl. apply H.
+   subst n. rewrite <- INR_IZR_INZ. apply (lt_INR 0).
+   apply Nat2Z.inj_lt. apply H. }
+  intros. apply (CReal_plus_lt_reg_r (-(IZR n))).
+  pose proof minus_IZR. unfold CReal_minus in H0.
+  repeat rewrite <- H0. unfold Zminus.
+  rewrite Z.add_opp_diag_r. apply posCase.
+  rewrite (Z.add_lt_mono_l _ _ n). ring_simplify. apply H.
+Qed.
+
+Lemma Z_R_minus : forall n m:Z, IZR n - IZR m == IZR (n - m).
+Proof.
+  intros z1 z2; unfold CReal_minus; unfold Z.sub.
+  rewrite plus_IZR, opp_IZR. reflexivity.
+Qed.
+
+Lemma lt_0_IZR : forall n:Z, 0 < IZR n -> (0 < n)%Z.
+Proof.
+  intro z; case z; simpl; intros.
+  elim (CRealLt_irrefl _ H).
+  easy. exfalso.
+  apply (CRealLt_asym 0 (IZR (Z.neg p))). exact H.
+  apply (IZR_lt (Z.neg p) 0). reflexivity.
+Qed.
+
+Lemma lt_IZR : forall n m:Z, IZR n < IZR m -> (n < m)%Z.
+Proof.
+  intros z1 z2 H; apply Z.lt_0_sub.
+  apply lt_0_IZR.
+  rewrite <- Z_R_minus. apply (CReal_plus_lt_reg_l (IZR z1)).
+  ring_simplify. exact H.
+Qed.
+
+Lemma IZR_le : forall n m:Z, (n <= m)%Z -> IZR n <= IZR m.
+Proof.
+  intros m n H. intro abs. apply (lt_IZR n m) in abs. omega.
+Qed.
 
 Lemma CReal_iterate_one : forall (n : nat),
     IZR (Z.of_nat n) == inject_Q (Z.of_nat n # 1).
@@ -2478,6 +2570,72 @@ Proof.
       simpl in maj. rewrite abs in maj. inversion maj.
 Qed.
 
+Lemma CReal_inv_r : forall (r:CReal) (rnz : r # 0),
+        r * ((/ r) rnz) == 1.
+Proof.
+  intros. rewrite CReal_mult_comm, CReal_inv_l.
+  reflexivity.
+Qed.
+
+Lemma CReal_inv_1 : forall nz : 1 # 0, (/ 1) nz == 1.
+Proof.
+  intros. rewrite <- (CReal_mult_1_l ((/1) nz)). rewrite CReal_inv_r.
+  reflexivity.
+Qed.
+
+Lemma CReal_inv_mult_distr :
+  forall r1 r2 (r1nz : r1 # 0) (r2nz : r2 # 0) (rmnz : (r1*r2) # 0),
+    (/ (r1 * r2)) rmnz == (/ r1) r1nz * (/ r2) r2nz.
+Proof.
+  intros. apply (CReal_mult_eq_reg_l r1). exact r1nz.
+  rewrite <- CReal_mult_assoc. rewrite CReal_inv_r. rewrite CReal_mult_1_l.
+  apply (CReal_mult_eq_reg_l r2). exact r2nz.
+  rewrite CReal_inv_r. rewrite <- CReal_mult_assoc.
+  rewrite (CReal_mult_comm r2 r1). rewrite CReal_inv_r.
+  reflexivity.
+Qed.
+
+Lemma Rinv_eq_compat : forall x y (rxnz : x # 0) (rynz : y # 0),
+    x == y
+    -> (/ x) rxnz == (/ y) rynz.
+Proof.
+  intros. apply (CReal_mult_eq_reg_l x). exact rxnz.
+ rewrite CReal_inv_r, H, CReal_inv_r. reflexivity.
+Qed.
+
+Lemma CReal_mult_lt_reg_l : forall r r1 r2, 0 < r -> r * r1 < r * r2 -> r1 < r2.
+Proof.
+  intros z x y H H0.
+  apply (CReal_mult_lt_compat_l ((/z) (or_intror H))) in H0.
+  repeat rewrite <- CReal_mult_assoc in H0. rewrite CReal_inv_l in H0.
+  repeat rewrite CReal_mult_1_l in H0. apply H0.
+  apply CReal_inv_0_lt_compat. exact H.
+Qed.
+
+Lemma CReal_mult_lt_reg_r : forall r r1 r2, 0 < r -> r1 * r < r2 * r -> r1 < r2.
+Proof.
+  intros.
+  apply CReal_mult_lt_reg_l with r.
+  exact H.
+  now rewrite 2!(CReal_mult_comm r).
+Qed.
+
+Lemma CReal_mult_eq_reg_r : forall r r1 r2, r1 * r == r2 * r -> r # 0 -> r1 == r2.
+Proof.
+  intros. apply (CReal_mult_eq_reg_l r). exact H0.
+  now rewrite 2!(CReal_mult_comm r).
+Qed.
+
+Lemma CReal_mult_eq_compat_l : forall r r1 r2, r1 == r2 -> r * r1 == r * r2.
+Proof.
+  intros. rewrite H. reflexivity.
+Qed.
+
+Lemma CReal_mult_eq_compat_r : forall r r1 r2, r1 == r2 -> r1 * r == r2 * r.
+Proof.
+  intros. rewrite H. reflexivity.
+Qed.
+
 Fixpoint pow (r:CReal) (n:nat) : CReal :=
   match n with
     | O => 1
@@ -2492,6 +2650,113 @@ Definition IQR (q:Q) : CReal :=
   end.
 Arguments IQR q%Q : simpl never.
 
+Lemma mult_IPR_IZR : forall (n:positive) (m:Z), IZR (Z.pos n * m) == IPR n * IZR m.
+Proof.
+  intros. rewrite mult_IZR. apply CReal_mult_eq_compat_r. reflexivity.
+Qed.
+
+Lemma plus_IQR : forall n m:Q, IQR (n + m) == IQR n + IQR m.
+Proof.
+  intros. destruct n,m; unfold Qplus,IQR; simpl.
+  rewrite plus_IZR. repeat rewrite mult_IZR.
+  setoid_replace ((/ IPR (Qden * Qden0)) (or_intror (IPR_pos (Qden * Qden0))))
+    with ((/ IPR Qden) (or_intror (IPR_pos Qden))
+          * (/ IPR Qden0) (or_intror (IPR_pos Qden0))).
+  rewrite CReal_mult_plus_distr_r.
+  repeat rewrite CReal_mult_assoc. rewrite <- (CReal_mult_assoc (IZR (Z.pos Qden))).
+  rewrite CReal_inv_r, CReal_mult_1_l.
+  rewrite (CReal_mult_comm ((/IPR Qden) (or_intror (IPR_pos Qden)))).
+  rewrite <- (CReal_mult_assoc (IZR (Z.pos Qden0))).
+  rewrite CReal_inv_r, CReal_mult_1_l. reflexivity. unfold IZR.
+  rewrite <- (CReal_inv_mult_distr
+                _ _ _ _ (or_intror (CReal_mult_lt_0_compat _ _ (IPR_pos _) (IPR_pos _)))).
+  apply Rinv_eq_compat. apply mult_IPR.
+Qed.
+
+Lemma IQR_pos : forall q:Q, Qlt 0 q -> 0 < IQR q.
+Proof.
+  intros. destruct q; unfold IQR.
+  apply CReal_mult_lt_0_compat. apply (IZR_lt 0).
+  unfold Qlt in H; simpl in H.
+  rewrite Z.mul_1_r in H. apply H.
+  apply CReal_inv_0_lt_compat. apply IPR_pos.
+Qed.
+
+Lemma opp_IQR : forall q:Q, IQR (- q) == - IQR q.
+Proof.
+  intros [a b]; unfold IQR; simpl.
+  rewrite CReal_opp_mult_distr_l.
+  rewrite opp_IZR. reflexivity.
+Qed.
+
+Lemma lt_IQR : forall n m:Q, IQR n < IQR m -> (n < m)%Q.
+Proof.
+  intros. destruct n,m; unfold IQR in H.
+  unfold Qlt; simpl. apply (CReal_mult_lt_compat_r (IPR Qden)) in H.
+  rewrite CReal_mult_assoc in H. rewrite CReal_inv_l in H.
+  rewrite CReal_mult_1_r in H. rewrite (CReal_mult_comm (IZR Qnum0)) in H.
+  apply (CReal_mult_lt_compat_l (IPR Qden0)) in H.
+  do 2 rewrite <- CReal_mult_assoc in H. rewrite CReal_inv_r in H.
+  rewrite CReal_mult_1_l in H.
+  rewrite (CReal_mult_comm (IZR Qnum0)) in H.
+  do 2 rewrite <- mult_IPR_IZR in H. apply lt_IZR in H.
+  rewrite Z.mul_comm. rewrite (Z.mul_comm Qnum0).
+  apply H. apply IPR_pos. apply IPR_pos.
+Qed.
+
+Lemma CReal_mult_le_compat_l_half : forall r r1 r2,
+    0 < r -> r1 <= r2 -> r * r1 <= r * r2.
+Proof.
+  intros. intro abs. apply (CReal_mult_lt_reg_l) in abs.
+  contradiction. apply H.
+Qed.
+
+Lemma IQR_lt : forall n m:Q, Qlt n m -> IQR n < IQR m.
+Proof.
+  intros. apply (CReal_plus_lt_reg_r (-IQR n)).
+  rewrite CReal_plus_opp_r. rewrite <- opp_IQR. rewrite <- plus_IQR.
+  apply IQR_pos. apply (Qplus_lt_l _ _ n).
+  ring_simplify. apply H.
+Qed.
+
+Lemma IQR_nonneg : forall q:Q, Qle 0 q -> 0 <= (IQR q).
+Proof.
+  intros [a b] H. unfold IQR;simpl.
+  apply (CRealLe_trans _ ((/ IPR b) (or_intror (IPR_pos b)) * 0)).
+  rewrite CReal_mult_0_r. apply CRealLe_refl.
+  rewrite (CReal_mult_comm (IZR a)). apply CReal_mult_le_compat_l_half.
+  apply CReal_inv_0_lt_compat. apply IPR_pos.
+  apply (IZR_le 0 a). unfold Qle in H; simpl in H.
+  rewrite Z.mul_1_r in H. apply H.
+Qed.
+
+Lemma IQR_le : forall n m:Q, Qle n m -> IQR n <= IQR m.
+Proof.
+  intros. intro abs. apply (CReal_plus_lt_compat_l (-IQR n)) in abs.
+  rewrite CReal_plus_opp_l,  <- opp_IQR, <- plus_IQR in abs.
+  apply IQR_nonneg in abs. contradiction. apply (Qplus_le_l _ _ n).
+  ring_simplify. apply H.
+Qed.
+
+Add Parametric Morphism : IQR
+    with signature Qeq ==> CRealEq
+      as IQR_morph.
+Proof.
+  intros. destruct x,y; unfold IQR; simpl.
+  unfold Qeq in H; simpl in H.
+  apply (CReal_mult_eq_reg_r (IZR (Z.pos Qden))).
+  2: right; apply IPR_pos.
+  rewrite CReal_mult_assoc. rewrite CReal_inv_l. rewrite CReal_mult_1_r.
+  rewrite (CReal_mult_comm (IZR Qnum0)).
+  apply (CReal_mult_eq_reg_l (IZR (Z.pos Qden0))).
+  right; apply IPR_pos.
+  rewrite <- CReal_mult_assoc, <- CReal_mult_assoc, CReal_inv_r.
+  rewrite CReal_mult_1_l.
+  repeat rewrite <- mult_IZR.
+  rewrite <- H. rewrite Zmult_comm. reflexivity.
+Qed.
+
+
 Lemma CReal_invQ : forall (b : positive) (pos : Qlt 0 (Z.pos b # 1)),
     CRealEq (CReal_inv (inject_Q (Z.pos b # 1)) (or_intror (CReal_injectQPos (Z.pos b # 1) pos)))
             (inject_Q (1 # b)).
@@ -2530,6 +2795,7 @@ Proof.
     discriminate.
 Qed.
 
+
 Close Scope R_scope_constr.
 
 Close Scope Q.
diff --git a/theories/Reals/ConstructiveRIneq.v b/theories/Reals/ConstructiveRIneq.v
index adffa9b719..e497b7d9bb 100644
--- a/theories/Reals/ConstructiveRIneq.v
+++ b/theories/Reals/ConstructiveRIneq.v
@@ -25,6 +25,8 @@ Local Open Scope R_scope_constr.
 
 (* Export all axioms *)
 
+Notation R := CReal (only parsing).
+Notation Req := CRealEq (only parsing).
 Notation Rplus_comm := CReal_plus_comm (only parsing).
 Notation Rplus_assoc := CReal_plus_assoc (only parsing).
 Notation Rplus_opp_r := CReal_plus_opp_r (only parsing).
@@ -40,12 +42,39 @@ Notation Rlt_trans := CRealLt_trans (only parsing).
 Notation Rplus_lt_compat_l := CReal_plus_lt_compat_l (only parsing).
 Notation Rmult_lt_compat_l := CReal_mult_lt_compat_l (only parsing).
 Notation Rmult_0_l := CReal_mult_0_l (only parsing).
+Notation INR := INR (only parsing).
+Notation IZR := IZR (only parsing).
+Notation IQR := IQR (only parsing).
 
 Hint Resolve Rplus_comm Rplus_assoc Rplus_opp_r Rplus_0_l
      Rmult_comm Rmult_assoc Rinv_l Rmult_1_l Rmult_plus_distr_l
      Rlt_0_1 Rlt_asym Rlt_trans Rplus_lt_compat_l Rmult_lt_compat_l
      Rmult_0_l : creal.
 
+Infix "==" := CRealEq : R_scope_constr.
+Infix "#" := CReal_appart : R_scope_constr.
+Infix "<" := CRealLt : R_scope_constr.
+Infix ">" := CRealGt : R_scope_constr.
+Infix "<=" := CRealLe : R_scope_constr.
+Infix ">=" := CRealGe : R_scope_constr.
+
+Notation "x <= y <= z" := (x <= y /\ y <= z) : R_scope_constr.
+Notation "x <= y < z"  := (x <= y /\ y <  z) : R_scope_constr.
+Notation "x < y < z"   := (x <  y /\ y <  z) : R_scope_constr.
+Notation "x < y <= z"  := (x <  y /\ y <= z) : R_scope_constr.
+
+Infix "+" := CReal_plus : R_scope_constr.
+Notation "- x" := (CReal_opp x) : R_scope_constr.
+Infix "-" := CReal_minus : R_scope_constr.
+Infix "*" := CReal_mult : R_scope_constr.
+Notation "/ x" := (CReal_inv x) (at level 35, right associativity) : R_scope_constr.
+
+Notation "0" := (inject_Q 0) : R_scope_constr.
+Notation "1" := (inject_Q 1) : R_scope_constr.
+Notation "2" := (IZR 2) : R_scope_constr.
+
+Add Ring CRealRing : CReal_isRing.
+
 
 (*********************************************************)
 (** ** Relation between orders and equality              *)
@@ -1928,167 +1957,6 @@ Proof.
   right. apply IPR_pos.
 Qed.
 
-Definition Rup_nat (x : CReal)
-  : { n : nat | x < INR n }.
-Proof.
-  intros. destruct (Rarchimedean x) as [p [maj _]].
-  destruct p.
-  - exists O. apply maj.
-  - exists (Pos.to_nat p). rewrite INR_IPR. apply maj.
-  - exists O. apply (CRealLt_trans _ (IZR (Z.neg p)) _ maj).
-    apply (IZR_lt _ 0). reflexivity.
-Qed.
-
-(* Sharpen the archimedean property : constructive versions of
-   the usual floor and ceiling functions.
-
-   n is a temporary parameter used for the recursion,
-   look at Ffloor below. *)
-Fixpoint Rfloor_pos (a : CReal) (n : nat) { struct n }
-  : 0 < a
-    -> a < INR n
-    -> { p : nat | INR p < a < INR p + 2 }.
-Proof.
-  (* Decreasing loop on n, until it is the first integer above a. *)
-  intros H H0. destruct n.
-  - exfalso. apply (CRealLt_asym 0 a); assumption.
-  - destruct n as [|p] eqn:des.
-    + (* n = 1 *) exists O. split.
-      apply H. rewrite Rplus_0_l. apply (CRealLt_trans a (1+0)).
-      rewrite Rplus_0_r. apply H0. apply Rplus_le_lt_compat.
-      apply Rle_refl. apply Rlt_0_1.
-    + (* n > 1 *)
-      destruct (linear_order_T (INR p) a (INR (S p))).
-      * rewrite <- Rplus_0_r, S_INR. apply Rplus_lt_compat_l.
-        apply Rlt_0_1.
-      * exists p. split. exact c.
-        rewrite S_INR, S_INR, Rplus_assoc in H0. exact H0.
-      * apply (Rfloor_pos a n H). rewrite des. apply c.
-Qed.
-
-Definition Rfloor (a : CReal)
-  : { p : Z | IZR p < a < IZR p + 2 }.
-Proof.
-  assert (forall x:CReal, 0 < x -> { n : nat | x < INR n }).
-  { intros. pose proof (Rarchimedean x) as [n [maj _]].
-    destruct n.
-    + exfalso. apply (CRealLt_asym 0 x); assumption.
-    + exists (Pos.to_nat p). rewrite INR_IPR. apply maj.
-    + exfalso. apply (CRealLt_asym 0 x). apply H.
-      apply (CRealLt_trans x (IZR (Z.neg p))). apply maj.
-      apply (Rplus_lt_reg_r (-IZR (Z.neg p))).
-      rewrite Rplus_opp_r. rewrite <- opp_IZR.
-      rewrite Rplus_0_l. apply (IZR_lt 0). reflexivity. }
-  destruct (linear_order_T 0 a 1 Rlt_0_1).
-  - destruct (H a c). destruct (Rfloor_pos a x c c0).
-    exists (Z.of_nat x0). rewrite <- INR_IZR_INZ. apply a0.
-  - apply (Rplus_lt_compat_r (-a)) in c.
-    rewrite Rplus_opp_r in c. destruct (H (1-a) c).
-    destruct (Rfloor_pos (1-a) x c c0).
-    exists (-(Z.of_nat x0 + 1))%Z. rewrite opp_IZR.
-    rewrite plus_IZR. simpl. split.
-    + rewrite <- (Ropp_involutive a). apply Ropp_gt_lt_contravar.
-      destruct a0 as [_ a0]. apply (Rplus_lt_reg_r 1).
-      rewrite Rplus_comm, Rplus_assoc. rewrite <- INR_IZR_INZ. apply a0.
-    + destruct a0 as [a0 _]. apply (Rplus_lt_compat_l a) in a0.
-      ring_simplify in a0. rewrite <- INR_IZR_INZ.
-      apply (Rplus_lt_reg_r (INR x0)). unfold IZR, IPR, IPR_2.
-      ring_simplify. exact a0.
-Qed.
-
-Lemma Qplus_same_denom : forall a b c, ((a # c) + (b # c) == (a+b) # c)%Q.
-Proof.
-  intros. unfold Qeq. simpl. rewrite Pos2Z.inj_mul. ring.
-Qed.
-
-(* A point in an archimedean field is the limit of a
-   sequence of rational numbers (n maps to the q between
-   a and a+1/n). This will yield a maximum
-   archimedean field, which is the field of real numbers. *)
-Definition FQ_dense_pos (a b : CReal)
-  : 0 < b
-    -> a < b -> { q : Q | a < IQR q < b }.
-Proof.
-  intros H H0.
-  assert (0 < b - a) as epsPos.
-  { apply (Rplus_lt_compat_r (-a)) in H0.
-    rewrite Rplus_opp_r in H0. apply H0. }
-  pose proof (Rarchimedean ((/(b-a)) (or_intror epsPos)))
-    as [n [maj _]].
-  destruct n as [|n|n].
-  - exfalso.
-    apply (Rmult_lt_compat_l (b-a)) in maj. 2: apply epsPos.
-    rewrite Rmult_0_r in maj. rewrite Rinv_r in maj.
-    apply (CRealLt_asym 0 1). apply Rlt_0_1. apply maj.
-    right. exact epsPos.
-  - (* 0 < n *)
-    destruct (Rfloor (IZR (2 * Z.pos n) * b)) as [p maj2].
-    exists (p # (2*n))%Q. split.
-    + apply (CRealLt_trans a (b - IQR (1 # n))).
-      apply (Rplus_lt_reg_r (IQR (1#n))).
-      unfold CReal_minus. rewrite Rplus_assoc. rewrite Rplus_opp_l.
-      rewrite Rplus_0_r. apply (Rplus_lt_reg_l (-a)).
-      rewrite <- Rplus_assoc. rewrite Rplus_opp_l. rewrite Rplus_0_l.
-      rewrite Rplus_comm. unfold IQR.
-      rewrite Rmult_1_l. apply (Rmult_lt_reg_l (IZR (Z.pos n))).
-      apply (IZR_lt 0). reflexivity. rewrite Rinv_r.
-      apply (Rmult_lt_compat_r (b-a)) in maj. rewrite Rinv_l in maj.
-      apply maj. exact epsPos.
-      right. apply IPR_pos.
-      apply (Rplus_lt_reg_r (IQR (1 # n))).
-      unfold CReal_minus. rewrite Rplus_assoc. rewrite Rplus_opp_l.
-      rewrite Rplus_0_r. rewrite <- plus_IQR.
-      destruct maj2 as [_ maj2].
-      setoid_replace ((p # 2 * n) + (1 # n))%Q
-        with ((p + 2 # 2 * n))%Q. unfold IQR.
-      apply (Rmult_lt_reg_r (IZR (Z.pos (2 * n)))).
-      apply (IZR_lt 0). reflexivity. rewrite Rmult_assoc.
-      rewrite Rinv_l. rewrite Rmult_1_r. rewrite Rmult_comm.
-      rewrite plus_IZR. apply maj2.
-      setoid_replace (1#n)%Q with (2#2*n)%Q. 2: reflexivity.
-      apply Qplus_same_denom.
-    + destruct maj2 as [maj2 _]. unfold IQR.
-      apply (Rmult_lt_reg_r (IZR (Z.pos (2 * n)))).
-      apply (IZR_lt 0). apply Pos2Z.is_pos. rewrite Rmult_assoc. rewrite Rinv_l.
-      rewrite Rmult_1_r. rewrite Rmult_comm. apply maj2.
-  - exfalso.
-    apply (Rmult_lt_compat_l (b-a)) in maj. 2: apply epsPos.
-    rewrite Rinv_r in maj. apply (CRealLt_asym 0 1). apply Rlt_0_1.
-    apply (CRealLt_trans 1 ((b - a) * IZR (Z.neg n)) _ maj).
-    rewrite <- (Rmult_0_r (b-a)).
-    apply Rmult_lt_compat_l. apply epsPos. apply (IZR_lt _ 0). reflexivity.
-    right. apply epsPos.
-Qed.
-
-Definition FQ_dense (a b : CReal)
-  : a < b
-    -> { q : Q | a < IQR q < b }.
-Proof.
-  intros H. destruct (linear_order_T a 0 b). apply H.
-  - destruct (FQ_dense_pos (-b) (-a)) as [q maj].
-    apply (Rplus_lt_compat_l (-a)) in c. rewrite Rplus_opp_l in c.
-    rewrite Rplus_0_r in c. apply c.
-    apply (Rplus_lt_compat_r (-a)) in H.
-    rewrite Rplus_opp_r in H.
-    apply (Rplus_lt_compat_l (-b)) in H. rewrite <- Rplus_assoc in H.
-    rewrite Rplus_opp_l in H. rewrite Rplus_0_l in H.
-    rewrite Rplus_0_r in H. apply H.
-    exists (-q)%Q. split.
-    + destruct maj as [_ maj].
-      apply (Rplus_lt_compat_r (-IQR q)) in maj.
-      rewrite Rplus_opp_r in maj. rewrite <- opp_IQR in maj.
-      apply (Rplus_lt_compat_l a) in maj. rewrite <- Rplus_assoc in maj.
-      rewrite Rplus_opp_r in maj. rewrite Rplus_0_l in maj.
-      rewrite Rplus_0_r in maj. apply maj.
-    + destruct maj as [maj _].
-      apply (Rplus_lt_compat_r (-IQR q)) in maj.
-      rewrite Rplus_opp_r in maj. rewrite <- opp_IQR in maj.
-      apply (Rplus_lt_compat_l b) in maj. rewrite <- Rplus_assoc in maj.
-      rewrite Rplus_opp_r in maj. rewrite Rplus_0_l in maj.
-      rewrite Rplus_0_r in maj. apply maj.
-  - apply FQ_dense_pos. apply c. apply H.
-Qed.
-
 
 (*********)
 Lemma Rmult_le_pos : forall r1 r2, 0 <= r1 -> 0 <= r2 -> 0 <= r1 * r2.
diff --git a/theories/Reals/ConstructiveRcomplete.v b/theories/Reals/ConstructiveRcomplete.v
index 9fb98a528b..06deff1bc1 100644
--- a/theories/Reals/ConstructiveRcomplete.v
+++ b/theories/Reals/ConstructiveRcomplete.v
@@ -12,13 +12,13 @@
 Require Import QArith_base.
 Require Import Qabs.
 Require Import ConstructiveCauchyReals.
-Require Import ConstructiveRIneq.
+Require Import Logic.ConstructiveEpsilon.
 
 Local Open Scope R_scope_constr.
 
 Lemma CReal_absSmall : forall x y : CReal,
     (exists n : positive, Qlt (2 # n)
-                             (proj1_sig x (Pos.to_nat n) - Qabs (proj1_sig y (Pos.to_nat n))))
+                         (proj1_sig x (Pos.to_nat n) - Qabs (proj1_sig y (Pos.to_nat n))))
     -> (CRealLt (CReal_opp x) y /\ CRealLt y x).
 Proof.
   intros. destruct H as [n maj]. split.
@@ -35,120 +35,181 @@ Proof.
     apply maj. apply Qplus_le_r. apply Qopp_le_compat. apply Qle_Qabs.
 Qed.
 
+Definition absSmall (a b : CReal) : Prop
+  := -b < a < b.
+
 Definition Un_cv_mod (un : nat -> CReal) (l : CReal) : Set
   := forall n : positive,
-    { p : nat | forall i:nat, le p i
-                     -> -IQR (1#n) < un i - l < IQR (1#n) }.
+    { p : nat | forall i:nat, le p i -> absSmall (un i - l) (IQR (1#n)) }.
 
 Lemma Un_cv_mod_eq : forall (v u : nat -> CReal) (s : CReal),
     (forall n:nat, u n == v n)
     -> Un_cv_mod u s -> Un_cv_mod v s.
 Proof.
   intros v u s seq H1 p. specialize (H1 p) as [N H0].
-  exists N. intros. rewrite <- seq. apply H0. apply H.
+  exists N. intros. unfold absSmall. rewrite <- seq. apply H0. apply H.
 Qed.
 
-Lemma IQR_double_inv : forall n : positive,
-    IQR (1 # 2*n) + IQR (1 # 2*n) == IQR (1 # n).
+Definition Un_cauchy_mod (un : nat -> CReal) : Set
+  := forall n : positive,
+    { p : nat | forall i j:nat, le p i
+                       -> le p j
+                       -> -IQR (1#n) < un i - un j < IQR (1#n) }.
+
+
+(* Sharpen the archimedean property : constructive versions of
+   the usual floor and ceiling functions.
+
+   n is a temporary parameter used for the recursion,
+   look at Ffloor below. *)
+Fixpoint Rfloor_pos (a : CReal) (n : nat) { struct n }
+  : 0 < a
+    -> a < INR n
+    -> { p : nat | INR p < a < INR p + 2 }.
 Proof.
-  intros. apply (Rmult_eq_reg_l (IPR (2*n))).
-  unfold IQR. do 2 rewrite Rmult_1_l.
-  rewrite Rmult_plus_distr_l, Rinv_r, IPR_double, Rmult_assoc, Rinv_r.
-  rewrite (Rmult_plus_distr_r 1 1). ring.
-  right. apply IPR_pos.
-  right. apply IPR_pos.
-  right. apply IPR_pos.
+  (* Decreasing loop on n, until it is the first integer above a. *)
+  intros H H0. destruct n.
+  - exfalso. apply (CRealLt_asym 0 a); assumption.
+  - destruct n as [|p] eqn:des.
+    + (* n = 1 *) exists O. split.
+      apply H. rewrite CReal_plus_0_l. apply (CRealLt_trans a (1+0)).
+      rewrite CReal_plus_comm, CReal_plus_0_l. apply H0.
+      apply CReal_plus_le_lt_compat.
+      apply CRealLe_refl. apply CRealLt_0_1.
+    + (* n > 1 *)
+      destruct (linear_order_T (INR p) a (INR (S p))).
+      * rewrite <- CReal_plus_0_l, S_INR, CReal_plus_comm. apply CReal_plus_lt_compat_l.
+        apply CRealLt_0_1.
+      * exists p. split. exact c.
+        rewrite S_INR, S_INR, CReal_plus_assoc in H0. exact H0.
+      * apply (Rfloor_pos a n H). rewrite des. apply c.
 Qed.
 
-Lemma CV_mod_plus :
-  forall (An Bn:nat -> CReal) (l1 l2:CReal),
-    Un_cv_mod An l1 -> Un_cv_mod Bn l2
-    -> Un_cv_mod (fun i:nat => An i + Bn i) (l1 + l2).
+Definition Rfloor (a : CReal)
+  : { p : Z | IZR p < a < IZR p + 2 }.
 Proof.
-  assert (forall x:CReal, x + x == 2*x) as double.
-  { intro. rewrite (Rmult_plus_distr_r 1 1), Rmult_1_l. reflexivity. }
-  intros. intros n.
-  destruct (H (2*n)%positive).
-  destruct (H0 (2*n)%positive).
-  exists (Nat.max x x0). intros.
-  setoid_replace (An i + Bn i - (l1 + l2))
-    with (An i - l1 + (Bn i - l2)). 2: ring.
-  rewrite <- IQR_double_inv. split.
-  - rewrite Ropp_plus_distr.
-    apply Rplus_lt_compat. apply a. apply (le_trans _ (max x x0)).
-    apply Nat.le_max_l. apply H1.
-    apply a0. apply (le_trans _ (max x x0)).
-    apply Nat.le_max_r. apply H1.
-  - apply Rplus_lt_compat. apply a. apply (le_trans _ (max x x0)).
-    apply Nat.le_max_l. apply H1.
-    apply a0. apply (le_trans _ (max x x0)).
-    apply Nat.le_max_r. apply H1.
+  assert (forall x:CReal, 0 < x -> { n : nat | x < INR n }).
+  { intros. pose proof (Rarchimedean x) as [n [maj _]].
+    destruct n.
+    + exfalso. apply (CRealLt_asym 0 x); assumption.
+    + exists (Pos.to_nat p). rewrite INR_IPR. apply maj.
+    + exfalso. apply (CRealLt_asym 0 x). apply H.
+      apply (CRealLt_trans x (IZR (Z.neg p))). apply maj.
+      apply (CReal_plus_lt_reg_l (-IZR (Z.neg p))).
+      rewrite CReal_plus_comm, CReal_plus_opp_r. rewrite <- opp_IZR.
+      rewrite CReal_plus_comm, CReal_plus_0_l.
+      apply (IZR_lt 0). reflexivity. }
+  destruct (linear_order_T 0 a 1 CRealLt_0_1).
+  - destruct (H a c). destruct (Rfloor_pos a x c c0).
+    exists (Z.of_nat x0). rewrite <- INR_IZR_INZ. apply a0.
+  - apply (CReal_plus_lt_compat_l (-a)) in c.
+    rewrite CReal_plus_comm, CReal_plus_opp_r, CReal_plus_comm in c.
+    destruct (H (1-a) c).
+    destruct (Rfloor_pos (1-a) x c c0).
+    exists (-(Z.of_nat x0 + 1))%Z. rewrite opp_IZR.
+    rewrite plus_IZR. simpl. split.
+    + rewrite <- (CReal_opp_involutive a). apply CReal_opp_gt_lt_contravar.
+      destruct a0 as [_ a0]. apply (CReal_plus_lt_reg_r 1).
+      rewrite CReal_plus_comm, CReal_plus_assoc. rewrite <- INR_IZR_INZ. apply a0.
+    + destruct a0 as [a0 _]. apply (CReal_plus_lt_compat_l a) in a0.
+      ring_simplify in a0. rewrite <- INR_IZR_INZ.
+      apply (CReal_plus_lt_reg_r (INR x0)). unfold IZR, IPR, IPR_2.
+      ring_simplify. exact a0.
 Qed.
 
-Lemma Un_cv_mod_const : forall x : CReal,
-    Un_cv_mod (fun _ => x) x.
+(* A point in an archimedean field is the limit of a
+   sequence of rational numbers (n maps to the q between
+   a and a+1/n). This will yield a maximum
+   archimedean field, which is the field of real numbers. *)
+Definition FQ_dense_pos (a b : CReal)
+  : 0 < b
+    -> a < b -> { q : Q | a < IQR q < b }.
 Proof.
-  intros. intro p. exists O. intros.
-  unfold CReal_minus. rewrite Rplus_opp_r.
-  split. rewrite <- Ropp_0.
-  apply Ropp_gt_lt_contravar. unfold IQR. rewrite Rmult_1_l.
-  apply Rinv_0_lt_compat. unfold IQR. rewrite Rmult_1_l.
-  apply Rinv_0_lt_compat.
+  intros H H0.
+  assert (0 < b - a) as epsPos.
+  { apply (CReal_plus_lt_compat_l (-a)) in H0.
+    rewrite CReal_plus_opp_l, CReal_plus_comm in H0.
+    apply H0. }
+  pose proof (Rarchimedean ((/(b-a)) (or_intror epsPos)))
+    as [n [maj _]].
+  destruct n as [|n|n].
+  - exfalso.
+    apply (CReal_mult_lt_compat_l (b-a)) in maj. 2: apply epsPos.
+    rewrite CReal_mult_0_r in maj. rewrite CReal_inv_r in maj.
+    apply (CRealLt_asym 0 1). apply CRealLt_0_1. apply maj.
+  - (* 0 < n *)
+    destruct (Rfloor (IZR (2 * Z.pos n) * b)) as [p maj2].
+    exists (p # (2*n))%Q. split.
+    + apply (CRealLt_trans a (b - IQR (1 # n))).
+      apply (CReal_plus_lt_reg_r (IQR (1#n))).
+      unfold CReal_minus. rewrite CReal_plus_assoc. rewrite CReal_plus_opp_l.
+      rewrite CReal_plus_0_r. apply (CReal_plus_lt_reg_l (-a)).
+      rewrite <- CReal_plus_assoc, CReal_plus_opp_l, CReal_plus_0_l.
+      rewrite CReal_plus_comm. unfold IQR.
+      rewrite CReal_mult_1_l. apply (CReal_mult_lt_reg_l (IZR (Z.pos n))).
+      apply (IZR_lt 0). reflexivity. rewrite CReal_inv_r.
+      apply (CReal_mult_lt_compat_l (b-a)) in maj.
+      rewrite CReal_inv_r, CReal_mult_comm in maj.
+      apply maj. exact epsPos.
+      apply (CReal_plus_lt_reg_r (IQR (1 # n))).
+      unfold CReal_minus. rewrite CReal_plus_assoc, CReal_plus_opp_l.
+      rewrite CReal_plus_0_r. rewrite <- plus_IQR.
+      destruct maj2 as [_ maj2].
+      setoid_replace ((p # 2 * n) + (1 # n))%Q
+        with ((p + 2 # 2 * n))%Q. unfold IQR.
+      apply (CReal_mult_lt_reg_r (IZR (Z.pos (2 * n)))).
+      apply (IZR_lt 0). reflexivity. rewrite CReal_mult_assoc.
+      rewrite CReal_inv_l. rewrite CReal_mult_1_r. rewrite CReal_mult_comm.
+      rewrite plus_IZR. apply maj2.
+      setoid_replace (1#n)%Q with (2#2*n)%Q. 2: reflexivity.
+      apply Qinv_plus_distr.
+    + destruct maj2 as [maj2 _]. unfold IQR.
+      apply (CReal_mult_lt_reg_r (IZR (Z.pos (2 * n)))).
+      apply (IZR_lt 0). apply Pos2Z.is_pos. rewrite CReal_mult_assoc, CReal_inv_l.
+      rewrite CReal_mult_1_r, CReal_mult_comm. apply maj2.
+  - exfalso.
+    apply (CReal_mult_lt_compat_l (b-a)) in maj. 2: apply epsPos.
+    rewrite CReal_inv_r in maj. apply (CRealLt_asym 0 1). apply CRealLt_0_1.
+    apply (CRealLt_trans 1 ((b - a) * IZR (Z.neg n)) _ maj).
+    rewrite <- (CReal_mult_0_r (b-a)).
+    apply CReal_mult_lt_compat_l. apply epsPos. apply (IZR_lt _ 0). reflexivity.
 Qed.
 
-(** Unicity of limit for convergent sequences *)
-Lemma UL_sequence_mod :
-  forall (Un:nat -> CReal) (l1 l2:CReal),
-    Un_cv_mod Un l1 -> Un_cv_mod Un l2 -> l1 == l2.
+Definition FQ_dense (a b : CReal)
+  : a < b
+    -> { q : Q | a < IQR q < b }.
 Proof.
-  assert (forall (Un:nat -> CReal) (l1 l2:CReal),
-             Un_cv_mod Un l1 -> Un_cv_mod Un l2
-             -> l1 <= l2).
-  - intros Un l1 l2; unfold Un_cv_mod; intros. intro abs.
-    assert (0 < l1 - l2) as epsPos.
-    { apply Rgt_minus. apply abs. }
-    destruct (Rup_nat ((/(l1-l2)) (or_intror epsPos))) as [n nmaj].
-    assert (lt 0 n) as nPos.
-    { apply (INR_lt 0). apply (Rlt_trans _ ((/ (l1 - l2)) (or_intror epsPos))).
-      2: apply nmaj. apply Rinv_0_lt_compat. }
-    specialize (H (2*Pos.of_nat n)%positive) as [i imaj].
-    specialize (H0 (2*Pos.of_nat n))%positive as [j jmaj].
-    specialize (imaj (max i j) (Nat.le_max_l _ _)) as [imaj _].
-    specialize (jmaj (max i j) (Nat.le_max_r _ _)) as [_ jmaj].
-    apply Ropp_gt_lt_contravar in imaj. rewrite Ropp_involutive in imaj.
-    unfold CReal_minus in imaj. rewrite Ropp_plus_distr in imaj.
-    rewrite Ropp_involutive in imaj. rewrite Rplus_comm in imaj.
-    apply (Rplus_lt_compat _ _ _ _ imaj) in jmaj.
-    clear imaj.
-    rewrite Rplus_assoc in jmaj. unfold CReal_minus in jmaj.
-    rewrite <- (Rplus_assoc (- Un (Init.Nat.max i j))) in jmaj.
-    rewrite Rplus_opp_l in jmaj.
-    rewrite <- double in jmaj. rewrite Rplus_0_l in jmaj.
-    rewrite (Rmult_plus_distr_r 1 1), Rmult_1_l, IQR_double_inv in jmaj.
-    unfold IQR in jmaj. rewrite Rmult_1_l in jmaj.
-    apply (Rmult_lt_compat_l (IPR (Pos.of_nat n))) in jmaj.
-    rewrite Rinv_r, <- INR_IPR, Nat2Pos.id in jmaj.
-    apply (Rmult_lt_compat_l (l1-l2)) in nmaj.
-    rewrite Rinv_r in nmaj. rewrite Rmult_comm in jmaj.
-    apply (CRealLt_asym 1 ((l1-l2)*INR n)); assumption.
-    right. apply epsPos. apply epsPos.
-    intro abss. subst n. inversion nPos.
-    right. apply IPR_pos. apply IPR_pos.
-  - intros. split; apply (H Un); assumption.
+  intros H. destruct (linear_order_T a 0 b). apply H.
+  - destruct (FQ_dense_pos (-b) (-a)) as [q maj].
+    apply (CReal_plus_lt_compat_l (-a)) in c. rewrite CReal_plus_opp_l in c.
+    rewrite CReal_plus_0_r in c. apply c.
+    apply (CReal_plus_lt_compat_l (-a)) in H.
+    rewrite CReal_plus_opp_l, CReal_plus_comm in H.
+    apply (CReal_plus_lt_compat_l (-b)) in H. rewrite <- CReal_plus_assoc in H.
+    rewrite CReal_plus_opp_l in H. rewrite CReal_plus_0_l in H.
+    rewrite CReal_plus_0_r in H. apply H.
+    exists (-q)%Q. split.
+    + destruct maj as [_ maj].
+      apply (CReal_plus_lt_compat_l (-IQR q)) in maj.
+      rewrite CReal_plus_opp_l, <- opp_IQR, CReal_plus_comm in maj.
+      apply (CReal_plus_lt_compat_l a) in maj. rewrite <- CReal_plus_assoc in maj.
+      rewrite CReal_plus_opp_r, CReal_plus_0_l in maj.
+      rewrite CReal_plus_0_r in maj. apply maj.
+    + destruct maj as [maj _].
+      apply (CReal_plus_lt_compat_l (-IQR q)) in maj.
+      rewrite CReal_plus_opp_l, <- opp_IQR, CReal_plus_comm in maj.
+      apply (CReal_plus_lt_compat_l b) in maj. rewrite <- CReal_plus_assoc in maj.
+      rewrite CReal_plus_opp_r in maj. rewrite CReal_plus_0_l in maj.
+      rewrite CReal_plus_0_r in maj. apply maj.
+  - apply FQ_dense_pos. apply c. apply H.
 Qed.
 
-Definition Un_cauchy_mod (un : nat -> CReal) : Set
-  := forall n : positive,
-    { p : nat | forall i j:nat, le p i
-                       -> le p j
-                       -> -IQR (1#n) < un i - un j < IQR (1#n) }.
-
 Definition RQ_limit : forall (x : CReal) (n:nat),
     { q:Q | x < IQR q < x + IQR (1 # Pos.of_nat n) }.
 Proof.
   intros x n. apply (FQ_dense x (x + IQR (1 # Pos.of_nat n))).
-  rewrite <- (Rplus_0_r x). rewrite Rplus_assoc.
-  apply Rplus_lt_compat_l. rewrite Rplus_0_l. apply IQR_pos.
+  rewrite <- (CReal_plus_0_r x). rewrite CReal_plus_assoc.
+  apply CReal_plus_lt_compat_l. rewrite CReal_plus_0_l. apply IQR_pos.
   reflexivity.
 Qed.
 
@@ -171,23 +232,24 @@ Proof.
   apply Nat.le_max_l. apply H0.
   split.
   - apply lt_IQR. unfold Qminus.
-    apply (Rlt_trans _ (xn p0 - (xn q + IQR (1 # 2 * p)))).
-    + unfold CReal_minus. rewrite Ropp_plus_distr. unfold CReal_minus.
-      rewrite <- Rplus_assoc.
-      apply (Rplus_lt_reg_r (IQR (1 # 2 * p))).
-      rewrite Rplus_assoc. rewrite Rplus_opp_l. rewrite Rplus_0_r.
+    apply (CRealLt_trans _ (xn p0 - (xn q + IQR (1 # 2 * p)))).
+    + unfold CReal_minus. rewrite CReal_opp_plus_distr. unfold CReal_minus.
+      rewrite <- CReal_plus_assoc.
+      apply (CReal_plus_lt_reg_r (IQR (1 # 2 * p))).
+      rewrite CReal_plus_assoc. rewrite CReal_plus_opp_l. rewrite CReal_plus_0_r.
       rewrite <- plus_IQR.
       setoid_replace (- (1 # p) + (1 # 2 * p))%Q with (- (1 # 2 * p))%Q.
       rewrite opp_IQR. exact H1.
       rewrite Qplus_comm.
       setoid_replace (1#p)%Q with (2 # 2 *p)%Q. rewrite Qinv_minus_distr.
       reflexivity. reflexivity.
-    + rewrite plus_IQR. apply Rplus_lt_compat.
+    + rewrite plus_IQR. apply CReal_plus_le_lt_compat.
+      apply CRealLt_asym.
       destruct (RQ_limit (xn p0) p0); simpl. apply a.
       destruct (RQ_limit (xn q) q); unfold proj1_sig.
-      rewrite opp_IQR. apply Ropp_gt_lt_contravar.
-      apply (Rlt_le_trans _ (xn q + IQR (1 # Pos.of_nat q))).
-      apply a. apply Rplus_le_compat_l. apply IQR_le.
+      rewrite opp_IQR. apply CReal_opp_gt_lt_contravar.
+      apply (CRealLt_Le_trans _ (xn q + IQR (1 # Pos.of_nat q))).
+      apply a. apply CReal_plus_le_compat_l. apply IQR_le.
       apply Z2Nat.inj_le. discriminate. discriminate.
       simpl. assert ((Pos.to_nat p~0 <= q)%nat).
       { apply (le_trans _ (Init.Nat.max k (2 * Pos.to_nat p))).
@@ -198,11 +260,12 @@ Proof.
       inversion H3. pose proof (Pos2Nat.is_pos (p~0)).
       rewrite H5 in H4. inversion H4.
   - apply lt_IQR. unfold Qminus.
-    apply (Rlt_trans _ (xn p0 + IQR (1 # 2 * p) - xn q)).
-    + rewrite plus_IQR. apply Rplus_lt_compat.
+    apply (CRealLt_trans _ (xn p0 + IQR (1 # 2 * p) - xn q)).
+    + rewrite plus_IQR. apply CReal_plus_le_lt_compat.
+      apply CRealLt_asym.
       destruct (RQ_limit (xn p0) p0); unfold proj1_sig.
-      apply (Rlt_le_trans _ (xn p0 + IQR (1 # Pos.of_nat p0))).
-      apply a. apply Rplus_le_compat_l. apply IQR_le.
+      apply (CRealLt_Le_trans _ (xn p0 + IQR (1 # Pos.of_nat p0))).
+      apply a. apply CReal_plus_le_compat_l. apply IQR_le.
       apply Z2Nat.inj_le. discriminate. discriminate.
       simpl. assert ((Pos.to_nat p~0 <= p0)%nat).
       { apply (le_trans _ (Init.Nat.max k (2 * Pos.to_nat p))).
@@ -212,12 +275,12 @@ Proof.
       rewrite Nat2Pos.id. apply H3. intro abs. subst p0.
       inversion H3. pose proof (Pos2Nat.is_pos (p~0)).
       rewrite H5 in H4. inversion H4.
-      rewrite opp_IQR. apply Ropp_gt_lt_contravar.
+      rewrite opp_IQR. apply CReal_opp_gt_lt_contravar.
       destruct (RQ_limit (xn q) q); simpl. apply a.
-    + unfold CReal_minus. rewrite (Rplus_comm (xn p0)).
-      rewrite Rplus_assoc.
-      apply (Rplus_lt_reg_l (- IQR (1 # 2 * p))).
-      rewrite <- Rplus_assoc. rewrite Rplus_opp_l. rewrite Rplus_0_l.
+    + unfold CReal_minus. rewrite (CReal_plus_comm (xn p0)).
+      rewrite CReal_plus_assoc.
+      apply (CReal_plus_lt_reg_l (- IQR (1 # 2 * p))).
+      rewrite <- CReal_plus_assoc. rewrite CReal_plus_opp_l. rewrite CReal_plus_0_l.
       rewrite <- opp_IQR. rewrite <- plus_IQR.
       setoid_replace (- (1 # 2 * p) + (1 # p))%Q with (1 # 2 * p)%Q.
       exact H2. rewrite Qplus_comm.
@@ -233,7 +296,7 @@ Lemma CReal_cv_self : forall (qn : nat -> Q) (x : CReal) (cvmod : positive -> na
 Proof.
   intros qn x cvmod H p.
   specialize (H (2*p)%positive). exists (cvmod (2*p)%positive).
-  intros p0 H0. unfold CReal_minus. rewrite FinjectQ_CReal.
+  intros p0 H0. unfold absSmall, CReal_minus. rewrite FinjectQ_CReal.
   setoid_replace (IQR (qn p0)) with (inject_Q (qn p0)).
   2: apply FinjectQ_CReal.
   apply CReal_absSmall.
@@ -246,12 +309,15 @@ Proof.
   2: destruct x; reflexivity.
   apply (Qle_lt_trans _ (1 # 2 * p)).
   unfold Qle; simpl. rewrite Pos2Z.inj_max. apply Z.le_max_l.
-  rewrite <- (Qplus_lt_r _ _ (-(1#p))). unfold Qminus. rewrite Qplus_assoc.
-  rewrite (Qplus_comm _ (1#p)). rewrite Qplus_opp_r. rewrite Qplus_0_l.
-  setoid_replace (- (1 # p) + (1 # 2 * p))%Q with (-(1 # 2 * p))%Q.
-  apply Qopp_lt_compat. apply H. apply H0.
-
-  rewrite Pos2Nat.inj_max.
+  rewrite <- (Qplus_lt_r
+               _ _ (Qabs
+     (qn p0 -
+      proj1_sig x
+                (2 * Pos.to_nat (Pos.max (4 * p) (Pos.of_nat (cvmod (2 * p)%positive))))%nat)
+                    -(1#2*p))).
+  ring_simplify.
+  setoid_replace (-1 * (1 # 2 * p) + (1 # p))%Q with (1 # 2 * p)%Q.
+  apply H. apply H0. rewrite Pos2Nat.inj_max.
   apply (le_trans _ (1 * Nat.max (Pos.to_nat (4 * p)) (Pos.to_nat (Pos.of_nat (cvmod (2 * p)%positive))))).
   destruct (cvmod (2*p)%positive). apply le_0_n. rewrite mult_1_l.
   rewrite Nat2Pos.id. 2: discriminate. apply Nat.le_max_r.
@@ -267,7 +333,7 @@ Lemma Un_cv_extens : forall (xn yn : nat -> CReal) (l : CReal),
     -> Un_cv_mod yn l.
 Proof.
   intros. intro p. destruct (H p) as [n cv]. exists n.
-  intros. unfold CReal_minus. rewrite <- (H0 i). apply cv. apply H1.
+  intros. unfold absSmall, CReal_minus. rewrite <- (H0 i). apply cv. apply H1.
 Qed.
 
 (* Q is dense in Archimedean fields, so all real numbers
@@ -284,8 +350,8 @@ Proof.
   - intros p n k H0 H1. destruct (H p); simpl in H0,H1.
     specialize (a n k H0 H1). apply Qabs_case.
     intros _. apply a. intros _.
-    rewrite <- (Qopp_involutive (1#p)). apply Qopp_lt_compat.
-    apply a.
+    apply (Qplus_lt_r _ _ (qn n -qn k-(1#p))). ring_simplify.
+    destruct a. ring_simplify in H2. exact H2.
   - exists (exist _ (fun n : nat =>
                        qn (increasing_modulus (fun p : positive => proj1_sig (H p)) n)) H0).
     apply (Un_cv_extens (fun n : nat => IQR (qn n))).
@@ -309,19 +375,20 @@ Proof.
   apply Nat.le_max_l. apply H.
   destruct (RQ_limit (xn p0) p0) as [q maj]; unfold proj1_sig in H0,H1.
   split.
-  - apply (Rlt_trans _ (IQR q - IQR (1 # 2 * p) - l)).
-    + unfold CReal_minus. rewrite (Rplus_comm (IQR q)).
-      apply (Rplus_lt_reg_l (IQR (1 # 2 * p))).
+  - apply (CRealLt_trans _ (IQR q - IQR (1 # 2 * p) - l)).
+    + unfold CReal_minus. rewrite (CReal_plus_comm (IQR q)).
+      apply (CReal_plus_lt_reg_l (IQR (1 # 2 * p))).
       ring_simplify. unfold CReal_minus. rewrite <- opp_IQR. rewrite <- plus_IQR.
       setoid_replace ((1 # 2 * p) + - (1 # p))%Q with (-(1#2*p))%Q.
       rewrite opp_IQR. apply H0.
       setoid_replace (1#p)%Q with (2 # 2*p)%Q.
       rewrite Qinv_minus_distr. reflexivity. reflexivity.
-    + unfold CReal_minus. apply Rplus_lt_compat_r.
-      apply (Rplus_lt_reg_r (IQR (1 # 2 * p))).
-      ring_simplify. rewrite Rplus_comm.
-      apply (Rlt_le_trans _ (xn p0 + IQR (1 # Pos.of_nat p0))).
-      apply maj. apply Rplus_le_compat_l.
+    + unfold CReal_minus.
+      do 2 rewrite <- (CReal_plus_comm (-l)). apply CReal_plus_lt_compat_l.
+      apply (CReal_plus_lt_reg_r (IQR (1 # 2 * p))).
+      ring_simplify. rewrite CReal_plus_comm.
+      apply (CRealLt_Le_trans _ (xn p0 + IQR (1 # Pos.of_nat p0))).
+      apply maj. apply CReal_plus_le_compat_l.
       apply IQR_le.
       apply Z2Nat.inj_le. discriminate. discriminate.
       simpl. assert ((Pos.to_nat p~0 <= p0)%nat).
@@ -332,12 +399,261 @@ Proof.
       rewrite Nat2Pos.id. apply H2. intro abs. subst p0.
       inversion H2. pose proof (Pos2Nat.is_pos (p~0)).
       rewrite H4 in H3. inversion H3.
-  - apply (Rlt_trans _ (IQR q - l)).
-    + apply Rplus_lt_compat_r. apply maj.
-    + apply (Rlt_trans _ (IQR (1 # 2 * p))).
+  - apply (CRealLt_trans _ (IQR q - l)).
+    + unfold CReal_minus. do 2 rewrite <- (CReal_plus_comm (-l)).
+      apply CReal_plus_lt_compat_l. apply maj.
+    + apply (CRealLt_trans _ (IQR (1 # 2 * p))).
       apply H1. apply IQR_lt.
       rewrite <- Qplus_0_r.
       setoid_replace (1#p)%Q with ((1#2*p)+(1#2*p))%Q.
       apply Qplus_lt_r. reflexivity.
-      rewrite Qplus_same_denom. reflexivity.
+      rewrite Qinv_plus_distr. reflexivity.
+Qed.
+
+Definition sig_forall_dec_T : Type
+  := forall (P : nat -> Prop), (forall n, {P n} + {~P n})
+                   -> {n | ~P n} + {forall n, P n}.
+
+Definition sig_not_dec_T : Type := forall P : Prop, {not (not P)} + {not P}.
+
+Definition is_upper_bound (E:CReal -> Prop) (m:CReal)
+  := forall x:CReal, E x -> x <= m.
+
+Definition is_lub (E:CReal -> Prop) (m:CReal) :=
+  is_upper_bound E m /\ (forall b:CReal, is_upper_bound E b -> m <= b).
+
+Lemma is_upper_bound_dec :
+  forall (E:CReal -> Prop) (x:CReal),
+    sig_forall_dec_T
+    -> sig_not_dec_T
+    -> { is_upper_bound E x } + { ~is_upper_bound E x }.
+Proof.
+  intros. destruct (X0 (~exists y:CReal, E y /\ x < y)).
+  - left. intros y H.
+    destruct (CRealLt_lpo_dec x y X). 2: exact n0.
+    exfalso. apply n. intro abs. apply abs.
+    exists y. split. exact H. exact c.
+  - right. intro abs. apply n. intros [y [H H0]].
+    specialize (abs y H). contradiction.
+Qed.
+
+Definition Rup_nat (x : CReal)
+  : { n : nat | x < INR n }.
+Proof.
+  intros. destruct (Rarchimedean x) as [p [maj _]].
+  destruct p.
+  - exists O. apply maj.
+  - exists (Pos.to_nat p). rewrite INR_IPR. apply maj.
+  - exists O. apply (CRealLt_trans _ (IZR (Z.neg p)) _ maj).
+    apply (IZR_lt _ 0). reflexivity.
+Qed.
+
+Lemma is_upper_bound_epsilon :
+  forall (E:CReal -> Prop),
+    sig_forall_dec_T
+    -> sig_not_dec_T
+    -> (exists x:CReal, is_upper_bound E x)
+    -> { n:nat | is_upper_bound E (INR n) }.
+Proof.
+  intros. apply constructive_indefinite_ground_description_nat.
+  - intro n. apply is_upper_bound_dec. exact X. exact X0.
+  - destruct H as [x H]. destruct (Rup_nat x). exists x0.
+    intros y ey. specialize (H y ey).
+    apply CRealLt_asym. apply (CRealLe_Lt_trans _ x); assumption.
+Qed.
+
+Lemma is_upper_bound_not_epsilon :
+  forall E:CReal -> Prop,
+    sig_forall_dec_T
+    -> sig_not_dec_T
+    -> (exists x : CReal, E x)
+    -> { m:nat | ~is_upper_bound E (-INR m) }.
+Proof.
+  intros E lpo sig_not_dec H.
+  apply constructive_indefinite_ground_description_nat.
+  - intro n. destruct (is_upper_bound_dec E (-INR n) lpo sig_not_dec).
+    right. intro abs. contradiction. left. exact n0.
+  - destruct H as [x H]. destruct (Rup_nat (-x)) as [n H0].
+    exists n. intro abs. specialize (abs x H).
+    apply abs. apply (CReal_plus_lt_reg_l (INR n-x)).
+    ring_simplify. exact H0.
+Qed.
+
+(* Decidable Dedekind cuts are Cauchy reals. *)
+Record DedekindDecCut : Type :=
+  {
+    DDupcut : Q -> Prop;
+    DDproper : forall q r : Q, (q == r -> DDupcut q -> DDupcut r)%Q;
+    DDlow : Q;
+    DDhigh : Q;
+    DDdec : forall q:Q, { DDupcut q } + { ~DDupcut q };
+    DDinterval : forall q r : Q, Qle q r -> DDupcut q -> DDupcut r;
+    DDhighProp : DDupcut DDhigh;
+    DDlowProp : ~DDupcut DDlow;
+  }.
+
+Lemma DDlow_below_up : forall (upcut : DedekindDecCut) (a b : Q),
+    DDupcut upcut a -> ~DDupcut upcut b -> Qlt b a.
+Proof.
+  intros. destruct (Qlt_le_dec b a). exact q.
+  exfalso. apply H0. apply (DDinterval upcut a).
+  exact q. exact H.
+Qed.
+
+Fixpoint DDcut_limit_fix (upcut : DedekindDecCut) (r : Q) (n : nat) :
+  Qlt 0 r
+  -> (DDupcut upcut (DDlow upcut + (Z.of_nat n#1) * r))
+  -> { q : Q | DDupcut upcut q /\ ~DDupcut upcut (q - r) }.
+Proof.
+  destruct n.
+  - intros. exfalso. simpl in H0.
+    apply (DDproper upcut _ (DDlow upcut)) in H0. 2: ring.
+    exact (DDlowProp upcut H0).
+  - intros. destruct (DDdec upcut (DDlow upcut + (Z.of_nat n # 1) * r)).
+    + exact (DDcut_limit_fix upcut r n H d).
+    + exists (DDlow upcut + (Z.of_nat (S n) # 1) * r)%Q. split.
+      exact H0. intro abs.
+      apply (DDproper upcut _ (DDlow upcut + (Z.of_nat n # 1) * r)) in abs.
+      contradiction.
+      rewrite Nat2Z.inj_succ. unfold Z.succ. rewrite <- Qinv_plus_distr.
+      ring.
+Qed.
+
+Lemma DDcut_limit : forall (upcut : DedekindDecCut) (r : Q),
+  Qlt 0 r
+  -> { q : Q | DDupcut upcut q /\ ~DDupcut upcut (q - r) }.
+Proof.
+  intros.
+  destruct (Qarchimedean ((DDhigh upcut - DDlow upcut)/r)) as [n nmaj].
+  apply (DDcut_limit_fix upcut r (Pos.to_nat n) H).
+  apply (Qmult_lt_r _ _ r) in nmaj. 2: exact H.
+  unfold Qdiv in nmaj.
+  rewrite <- Qmult_assoc, (Qmult_comm (/r)), Qmult_inv_r, Qmult_1_r in nmaj.
+  apply (DDinterval upcut (DDhigh upcut)). 2: exact (DDhighProp upcut).
+  apply Qlt_le_weak. apply (Qplus_lt_r _ _ (-DDlow upcut)).
+  rewrite Qplus_assoc, <- (Qplus_comm (DDlow upcut)), Qplus_opp_r,
+  Qplus_0_l, Qplus_comm.
+  rewrite positive_nat_Z. exact nmaj.
+  intros abs. rewrite abs in H. exact (Qlt_irrefl 0 H).
+Qed.
+
+Lemma glb_dec_Q : forall upcut : DedekindDecCut,
+    { x : CReal | forall r:Q, (x < IQR r -> DDupcut upcut r)
+                         /\ (IQR r < x -> ~DDupcut upcut r) }.
+Proof.
+  intros.
+  assert (forall a b : Q, Qle a b -> Qle (-b) (-a)).
+  { intros. apply (Qplus_le_l _ _ (a+b)). ring_simplify. exact H. }
+  assert (QCauchySeq (fun n:nat => proj1_sig (DDcut_limit
+                                           upcut (1#Pos.of_nat n) (eq_refl _)))
+                     Pos.to_nat).
+  { intros p i j pi pj.
+    destruct (DDcut_limit upcut (1 # Pos.of_nat i) eq_refl),
+    (DDcut_limit upcut (1 # Pos.of_nat j) eq_refl); unfold proj1_sig.
+    apply Qabs_case. intros.
+    apply (Qplus_lt_l _ _ (x0- (1#p))). ring_simplify.
+    setoid_replace (x + -1 * (1 # p))%Q with (x - (1 # p))%Q.
+    2: ring. apply (Qle_lt_trans _ (x- (1#Pos.of_nat i))).
+    apply Qplus_le_r. apply H.
+    apply Z2Nat.inj_le. discriminate. discriminate. simpl.
+    rewrite Nat2Pos.id. exact pi. intro abs.
+    subst i. inversion pi. pose proof (Pos2Nat.is_pos p).
+    rewrite H2 in H1. inversion H1.
+    apply (DDlow_below_up upcut). apply a0. apply a.
+    intros.
+    apply (Qplus_lt_l _ _ (x- (1#p))). ring_simplify.
+    setoid_replace (x0 + -1 * (1 # p))%Q with (x0 - (1 # p))%Q.
+    2: ring. apply (Qle_lt_trans _ (x0- (1#Pos.of_nat j))).
+    apply Qplus_le_r. apply H.
+    apply Z2Nat.inj_le. discriminate. discriminate. simpl.
+    rewrite Nat2Pos.id. exact pj. intro abs.
+    subst j. inversion pj. pose proof (Pos2Nat.is_pos p).
+    rewrite H2 in H1. inversion H1.
+    apply (DDlow_below_up upcut). apply a. apply a0. }
+  pose (exist (fun qn => QSeqEquiv qn qn Pos.to_nat) _ H0) as l.
+  exists l. split.
+  - intros. (* find an upper point between the limit and r *)
+    rewrite FinjectQ_CReal in H1. destruct H1 as [p pmaj].
+    unfold l,proj1_sig in pmaj.
+    destruct (DDcut_limit upcut (1 # Pos.of_nat (Pos.to_nat p)) eq_refl) as [q qmaj]
+    ; simpl in pmaj.
+    apply (DDinterval upcut q). 2: apply qmaj.
+    apply (Qplus_lt_l _ _ q) in pmaj. ring_simplify in pmaj.
+    apply (Qle_trans _ ((2#p) + q)).
+    apply (Qplus_le_l _ _ (-q)). ring_simplify. discriminate.
+    apply Qlt_le_weak. exact pmaj.
+  - intros H1 abs.
+    rewrite FinjectQ_CReal in H1. destruct H1 as [p pmaj].
+    unfold l,proj1_sig in pmaj.
+    destruct (DDcut_limit upcut (1 # Pos.of_nat (Pos.to_nat p)) eq_refl) as [q qmaj]
+    ; simpl in pmaj.
+    rewrite Pos2Nat.id in qmaj.
+    apply (Qplus_lt_r _ _ (r - (2#p))) in pmaj. ring_simplify in pmaj.
+    destruct qmaj. apply H2.
+    apply (DDinterval upcut r). 2: exact abs.
+    apply Qlt_le_weak, (Qlt_trans _ (-1*(2#p) + q) _ pmaj).
+    apply (Qplus_lt_l _ _ ((2#p) -q)). ring_simplify.
+    setoid_replace (-1 * (1 # p))%Q with (-(1#p))%Q.
+    2: ring. rewrite Qinv_minus_distr. reflexivity.
+Qed.
+
+Lemma is_upper_bound_glb :
+  forall (E:CReal -> Prop),
+    sig_not_dec_T
+    -> sig_forall_dec_T
+    -> (exists x : CReal, E x)
+    -> (exists x : CReal, is_upper_bound E x)
+    -> { x : CReal | forall r:Q, (x < IQR r -> is_upper_bound E (IQR r))
+                           /\ (IQR r < x -> ~is_upper_bound E (IQR r)) }.
+Proof.
+  intros.
+  destruct (is_upper_bound_epsilon E X0 X H0) as [a luba].
+  destruct (is_upper_bound_not_epsilon E X0 X H) as [b glbb].
+  pose (fun q => is_upper_bound E (IQR q)) as upcut.
+  assert (forall q:Q, { upcut q } + { ~upcut q } ).
+  { intro q. apply is_upper_bound_dec. exact X0. exact X. }
+  assert (forall q r : Q, (q <= r)%Q -> upcut q -> upcut r).
+  { intros. intros x Ex. specialize (H3 x Ex). intro abs.
+    apply H3. apply (CRealLe_Lt_trans _ (IQR r)). 2: exact abs.
+    apply IQR_le. exact H2. }
+  assert (upcut (Z.of_nat a # 1)%Q).
+  { intros x Ex. unfold IQR. rewrite CReal_inv_1, CReal_mult_1_r.
+    specialize (luba x Ex). rewrite <- INR_IZR_INZ. exact luba. }
+  assert (~upcut (- Z.of_nat b # 1)%Q).
+  { intros abs. apply glbb. intros x Ex.
+    specialize (abs x Ex). unfold IQR in abs.
+    rewrite CReal_inv_1, CReal_mult_1_r, opp_IZR, <- INR_IZR_INZ in abs.
+    exact abs. }
+  assert (forall q r : Q, (q == r)%Q -> upcut q -> upcut r).
+  { intros. intros x Ex. specialize (H6 x Ex). rewrite <- H5. exact H6. }
+  destruct (glb_dec_Q (Build_DedekindDecCut
+                         upcut H5 (-Z.of_nat b # 1)%Q (Z.of_nat a # 1)
+                         H1 H2 H3 H4)).
+  simpl in a0. exists x. intro r. split.
+  - intros. apply a0. exact H6.
+  - intros H6 abs. specialize (a0 r) as [_ a0]. apply a0.
+    exact H6. exact abs.
+Qed.
+
+Lemma is_upper_bound_closed :
+  forall (E:CReal -> Prop) (sig_forall_dec : sig_forall_dec_T)
+    (sig_not_dec : sig_not_dec_T)
+    (Einhab : exists x : CReal, E x)
+    (Ebound : exists x : CReal, is_upper_bound E x),
+    is_lub
+      E (proj1_sig (is_upper_bound_glb
+                      E sig_not_dec sig_forall_dec Einhab Ebound)).
+Proof.
+  intros. split.
+  - intros x Ex.
+    destruct (is_upper_bound_glb E sig_not_dec sig_forall_dec Einhab Ebound); simpl.
+    intro abs. destruct (FQ_dense x0 x abs) as [q [qmaj H]].
+    specialize (a q) as [a _]. specialize (a qmaj x Ex).
+    contradiction.
+  - intros.
+    destruct (is_upper_bound_glb E sig_not_dec sig_forall_dec Einhab Ebound); simpl.
+    intro abs. destruct (FQ_dense b x abs) as [q [qmaj H0]].
+    specialize (a q) as [_ a]. apply a. exact H0.
+    intros y Ey. specialize (H y Ey). intro abs2.
+    apply H. exact (CRealLt_trans _ (IQR q) _ qmaj abs2).
 Qed.
diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v
index 8379829037..fd375e67be 100644
--- a/theories/Reals/Raxioms.v
+++ b/theories/Reals/Raxioms.v
@@ -14,6 +14,7 @@
 
 Require Export ZArith_base.
 Require Import ConstructiveCauchyReals.
+Require Import ConstructiveRcomplete.
 Require Export Rdefinitions.
 Declare Scope R_scope.
 Local Open Scope R_scope.
@@ -349,12 +350,27 @@ Definition is_lub (E:R -> Prop) (m:R) :=
   is_upper_bound E m /\ (forall b:R, is_upper_bound E b -> m <= b).
 
 (**********)
-(* This axiom can be proved by excluded middle in sort Set.
-   For this, define a sequence by dichotomy, using excluded middle
-   to know whether the current point majorates E or not.
-   Then conclude by the Cauchy-completeness of R, which is proved
-   constructively. *)
-Axiom
-  completeness :
+Lemma completeness :
     forall E:R -> Prop,
       bound E -> (exists x : R, E x) -> { m:R | is_lub E m }.
+Proof.
+  intros. pose (fun x:CReal => E (Rabst x)) as Er.
+  assert (exists x : CReal, Er x) as Einhab.
+  { destruct H0. exists (Rrepr x). unfold Er.
+    replace (Rabst (Rrepr x)) with x. exact H0.
+    apply Rquot1. rewrite Rquot2. reflexivity. }
+  assert (exists x : CReal, ConstructiveRcomplete.is_upper_bound Er x) as Ebound.
+  { destruct H. exists (Rrepr x). intros y Ey. rewrite <- (Rquot2 y).
+    apply Rrepr_le. apply H. exact Ey. }
+  pose proof (is_upper_bound_closed Er sig_forall_dec sig_not_dec
+                                    Einhab Ebound).
+  destruct (is_upper_bound_glb
+              Er sig_not_dec sig_forall_dec Einhab Ebound); simpl in H1.
+  exists (Rabst x). split.
+  intros y Ey. apply Rrepr_le. rewrite Rquot2. apply H1.
+  unfold Er. replace (Rabst (Rrepr y)) with y. exact Ey.
+  apply Rquot1. rewrite Rquot2. reflexivity.
+  intros. destruct H1. apply Rrepr_le. rewrite Rquot2.
+  apply H3. intros y Ey. rewrite <- Rquot2.
+  apply Rrepr_le, H2, Ey.
+Qed.
diff --git a/theories/Reals/Rdefinitions.v b/theories/Reals/Rdefinitions.v
index 03eb6c8b44..025192203e 100644
--- a/theories/Reals/Rdefinitions.v
+++ b/theories/Reals/Rdefinitions.v
@@ -33,6 +33,8 @@ Axiom sig_forall_dec
   : forall (P : nat -> Prop), (forall n, {P n} + {~P n})
                    -> {n | ~P n} + {forall n, P n}.
 
+Axiom sig_not_dec : forall P : Prop, {not (not P)} + {not P}.
+
 Axiom Rabst : CReal -> R.
 Axiom Rrepr : R -> CReal.
 Axiom Rquot1 : forall x y:R, CRealEq (Rrepr x) (Rrepr y) -> x = y.
@@ -151,30 +153,11 @@ Definition IZR (z:Z) : R :=
   end.
 Arguments IZR z%Z : simpl never.
 
-Lemma CRealLt_dec : forall x y : CReal, { CRealLt x y } + { ~CRealLt x y }.
-Proof.
-  intros.
-  destruct (sig_forall_dec
-              (fun n:nat => Qle (proj1_sig y (S n) - proj1_sig x (S n)) (2 # Pos.of_nat (S n)))).
-  - intro n. destruct (Qlt_le_dec (2 # Pos.of_nat (S n))
-                                  (proj1_sig y (S n) - proj1_sig x (S n))).
-    right. apply Qlt_not_le. exact q. left. exact q.
-  - left. destruct s as [n nmaj]. exists (Pos.of_nat (S n)).
-    rewrite Nat2Pos.id. apply Qnot_le_lt. exact nmaj. discriminate.
-  - right. intro abs. destruct abs as [n majn].
-    specialize (q (pred (Pos.to_nat n))).
-    replace (S (pred (Pos.to_nat n))) with (Pos.to_nat n) in q.
-    rewrite Pos2Nat.id in q.
-    pose proof (Qle_not_lt _ _ q). contradiction.
-    symmetry. apply Nat.succ_pred. intro abs.
-    pose proof (Pos2Nat.is_pos n). rewrite abs in H. inversion H.
-Qed.
-
 Lemma total_order_T : forall r1 r2:R, {Rlt r1 r2} + {r1 = r2} + {Rlt r2 r1}.
 Proof.
-  intros. destruct (CRealLt_dec (Rrepr r1) (Rrepr r2)).
+  intros. destruct (CRealLt_lpo_dec (Rrepr r1) (Rrepr r2) sig_forall_dec).
   - left. left. rewrite RbaseSymbolsImpl.Rlt_def. exact c.
-  - destruct (CRealLt_dec (Rrepr r2) (Rrepr r1)).
+  - destruct (CRealLt_lpo_dec (Rrepr r2) (Rrepr r1) sig_forall_dec).
     + right. rewrite RbaseSymbolsImpl.Rlt_def. exact c.
     + left. right. apply Rquot1. split; assumption.
 Qed.
-- 
cgit v1.2.3