Merge PR #10632: Prove the completeness of real numbers from logical axiom sig_not_dec

Reviewed-by: herbelin

10 files changed, 2479 insertions, 864 deletions

diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index dcfe4a08f3..cc91776a4d 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -514,9 +514,11 @@ through the <tt>Require Import</tt> command.</p>
   </dt>
   <dd>
     theories/Reals/Rdefinitions.v
+    theories/Reals/ConstructiveReals.v
     theories/Reals/ConstructiveCauchyReals.v
     theories/Reals/Raxioms.v
     theories/Reals/ConstructiveRIneq.v
+    theories/Reals/ConstructiveRealsLUB.v
     theories/Reals/RIneq.v
     theories/Reals/DiscrR.v
     theories/Reals/ROrderedType.v
diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v
index 21bea6c315..b60feb9256 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 | q < Z.pos p # 1 }.
+Proof.
+  intros. destruct q as [a b]. destruct a.
+  - exists xH. reflexivity.
+  - exists (p+1)%positive. apply (Z.lt_le_trans _ (Z.pos (p+1))).
+    simpl. rewrite Pos.mul_1_r.
+    apply Z.lt_succ_diag_r. simpl. 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.
+Defined.
+
 (** 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,
+    0 < a -> 0 < b -> (a < b <-> /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..004854e751 100644
--- a/theories/Reals/ConstructiveCauchyReals.v
+++ b/theories/Reals/ConstructiveCauchyReals.v
@@ -13,6 +13,7 @@ Require Import QArith.
 Require Import Qabs.
 Require Import Qround.
 Require Import Logic.ConstructiveEpsilon.
+Require CMorphisms.
 
 Open Scope Q.
 
@@ -24,95 +25,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).
@@ -290,105 +205,36 @@ Qed.
 Definition CReal : Set
   := { x : (nat -> Q) | QCauchySeq x Pos.to_nat }.
 
-Declare Scope R_scope_constr.
+Declare Scope CReal_scope.
 
 (* Declare Scope R_scope with Key R *)
-Delimit Scope R_scope_constr with CReal.
+Delimit Scope CReal_scope with CReal.
 
 (* Automatically open scope R_scope for arguments of type R *)
-Bind Scope R_scope_constr with CReal.
+Bind Scope CReal_scope 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.
+Open Scope CReal_scope.
 
 
 (* So QSeqEquiv is the equivalence relation of this constructive pre-order *)
-Definition CRealLt (x y : CReal) : Prop
+Definition CRealLt (x y : CReal) : Set
+  := { n : positive |  Qlt (2 # n)
+                           (proj1_sig y (Pos.to_nat n) - proj1_sig x (Pos.to_nat n)) }.
+
+Definition CRealLtProp (x y : CReal) : Prop
   := exists n : positive, Qlt (2 # n)
                          (proj1_sig y (Pos.to_nat n) - proj1_sig x (Pos.to_nat n)).
 
 Definition CRealGt (x y : CReal) := CRealLt y x.
-Definition CReal_appart (x y : CReal) := CRealLt x y \/ CRealLt y x.
+Definition CReal_appart (x y : CReal) := sum (CRealLt x y) (CRealLt y x).
 
-Infix "<" := CRealLt : R_scope_constr.
-Infix ">" := CRealGt : R_scope_constr.
-Infix "#" := CReal_appart : R_scope_constr.
+Infix "<" := CRealLt : CReal_scope.
+Infix ">" := CRealGt : CReal_scope.
+Infix "#" := CReal_appart : CReal_scope.
 
 (* This Prop can be extracted as a sigma type *)
 Lemma CRealLtEpsilon : forall x y : CReal,
-    x < y
-    -> { n : positive | Qlt (2 # n)
-                           (proj1_sig y (Pos.to_nat n) - proj1_sig x (Pos.to_nat n)) }.
+    CRealLtProp x y -> x < y.
 Proof.
   intros.
   assert (exists n : nat, n <> O
@@ -409,25 +255,55 @@ Proof.
                     (proj1_sig y (S n) - proj1_sig x (S n))); assumption.
 Qed.
 
+Lemma CRealLtForget : forall x y : CReal,
+    x < y -> CRealLtProp x y.
+Proof.
+  intros. destruct H. exists x0. exact q.
+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 -> False).
+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.
+  := (CRealLt x y -> False) /\ (CRealLt y x -> False).
 
-Infix "==" := CRealEq : R_scope_constr.
+Infix "==" := CRealEq : CReal_scope.
 
 (* Alias the large order *)
 Definition CRealLe (x y : CReal) : Prop
-  := ~CRealLt y x.
+  := CRealLt y x -> False.
 
 Definition CRealGe (x y : CReal) := CRealLe y x.
 
-Infix "<=" := CRealLe : R_scope_constr.
-Infix ">=" := CRealGe : R_scope_constr.
+Infix "<=" := CRealLe : CReal_scope.
+Infix ">=" := CRealGe : CReal_scope.
 
-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.
+Notation "x <= y <= z" := (x <= y /\ y <= z) : CReal_scope.
+Notation "x <= y < z"  := (prod (x <= y) (y < z)) : CReal_scope.
+Notation "x < y < z"   := (prod (x < y) (y < z)) : CReal_scope.
+Notation "x < y <= z"  := (prod (x < y) (y <= z)) : CReal_scope.
 
 Lemma CRealLe_not_lt : forall x y : CReal,
     (forall n:positive, Qle (proj1_sig x (Pos.to_nat n) - proj1_sig y (Pos.to_nat n))
@@ -465,6 +341,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)
@@ -520,8 +469,8 @@ Qed.
 
 Lemma CRealLt_above : forall (x y : CReal),
     CRealLt x y
-    -> exists k : positive, forall p:positive,
-          Pos.le k p -> Qlt (2 # k) (proj1_sig y (Pos.to_nat p) - proj1_sig x (Pos.to_nat p)).
+    -> { k : positive | forall p:positive,
+          Pos.le k p -> Qlt (2 # k) (proj1_sig y (Pos.to_nat p) - proj1_sig x (Pos.to_nat p)) }.
 Proof.
   intros x y [n maj].
   pose proof (CRealLt_aboveSig x y n maj).
@@ -565,20 +514,15 @@ 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).
+Lemma CRealLt_irrefl : forall x:CReal, x < x -> False.
 Proof.
   intros x abs. exact (CRealLt_asym x x abs abs).
 Qed.
@@ -600,10 +544,10 @@ Proof.
 Qed.
 
 Lemma CRealLt_dec : forall x y z : CReal,
-    CRealLt x y -> { CRealLt x z } + { CRealLt z y }.
+    CRealLt x y -> CRealLt x z  +  CRealLt z y.
 Proof.
   intros [xn limx] [yn limy] [zn limz] clt.
-  destruct (CRealLtEpsilon _ _ clt) as [n inf].
+  destruct clt as [n inf].
   unfold proj1_sig in inf.
   remember (yn (Pos.to_nat n) - xn (Pos.to_nat n) - (2 # n)) as eps.
   assert (Qlt 0 eps) as epsPos.
@@ -656,9 +600,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.
@@ -680,7 +625,7 @@ Proof.
       apply Qinv_lt_contravar. reflexivity. apply epsPos. apply kmaj.
       unfold Qeq. simpl. rewrite Pos.mul_1_r. reflexivity.
       field. assumption.
-Qed.
+Defined.
 
 Definition linear_order_T x y z := CRealLt_dec x z y.
 
@@ -692,13 +637,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.
@@ -720,11 +671,16 @@ Add Parametric Relation : CReal CRealEq
     transitivity proved by CRealEq_trans
       as CRealEq_rel.
 
-Add Parametric Morphism : CRealLt
-    with signature CRealEq ==> CRealEq ==> iff
-      as CRealLt_morph.
+Instance CRealEq_relT : CRelationClasses.Equivalence CRealEq.
+Proof.
+  split. exact CRealEq_refl. exact CRealEq_sym. exact CRealEq_trans.
+Qed.
+
+Instance CRealLt_morph
+  : CMorphisms.Proper
+      (CMorphisms.respectful CRealEq (CMorphisms.respectful CRealEq CRelationClasses.iffT)) CRealLt.
 Proof.
-  intros. destruct H, H0. split.
+  intros x y H x0 y0 H0. destruct H, H0. split.
   - intro. destruct (CRealLt_dec x x0 y). assumption.
     contradiction. destruct (CRealLt_dec y x0 y0).
     assumption. assumption. contradiction.
@@ -733,22 +689,22 @@ Proof.
     assumption. assumption. contradiction.
 Qed.
 
-Add Parametric Morphism : CRealGt
-    with signature CRealEq ==> CRealEq ==> iff
-      as CRealGt_morph.
+Instance CRealGt_morph
+  : CMorphisms.Proper
+      (CMorphisms.respectful CRealEq (CMorphisms.respectful CRealEq CRelationClasses.iffT)) CRealGt.
 Proof.
-  intros. unfold CRealGt. apply CRealLt_morph; assumption.
+  intros x y H x0 y0 H0. apply CRealLt_morph; assumption.
 Qed.
 
-Add Parametric Morphism : CReal_appart
-    with signature CRealEq ==> CRealEq ==> iff
-      as CReal_appart_morph.
+Instance CReal_appart_morph
+  : CMorphisms.Proper
+      (CMorphisms.respectful CRealEq (CMorphisms.respectful CRealEq CRelationClasses.iffT)) CReal_appart.
 Proof.
   split.
-  - intros. destruct H1. left. rewrite <- H0, <- H. exact H1.
-    right. rewrite <- H0, <- H. exact H1.
-  - intros. destruct H1. left. rewrite H0, H. exact H1.
-    right. rewrite H0, H. exact H1.
+  - intros. destruct H1. left. rewrite <- H0, <- H. exact c.
+    right. rewrite <- H0, <- H. exact c.
+  - intros. destruct H1. left. rewrite H0, H. exact c.
+    right. rewrite H0, H. exact c.
 Qed.
 
 Add Parametric Morphism : CRealLe
@@ -818,8 +774,8 @@ Proof.
   intro q. exists (fun n => q). apply ConstCauchy.
 Defined.
 
-Notation "0" := (inject_Q 0) : R_scope_constr.
-Notation "1" := (inject_Q 1) : R_scope_constr.
+Notation "0" := (inject_Q 0) : CReal_scope.
+Notation "1" := (inject_Q 1) : CReal_scope.
 
 Lemma CRealLt_0_1 : CRealLt (inject_Q 0) (inject_Q 1).
 Proof.
@@ -948,7 +904,13 @@ Proof.
     apply le_0_n. apply H1. apply le_refl.
 Defined.
 
-Infix "+" := CReal_plus : R_scope_constr.
+Infix "+" := CReal_plus : CReal_scope.
+
+Lemma CReal_plus_nth : forall (x y : CReal) (n : nat),
+    proj1_sig (x + y) n = Qplus (proj1_sig x (2*n)%nat) (proj1_sig y (2*n)%nat).
+Proof.
+  intros. destruct x,y; reflexivity.
+Qed.
 
 Lemma CReal_plus_unfold : forall (x y : CReal),
     QSeqEquiv (proj1_sig (CReal_plus x y))
@@ -981,15 +943,15 @@ 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.
+Notation "- x" := (CReal_opp x) : CReal_scope.
 
 Definition CReal_minus (x y : CReal) : CReal
   := CReal_plus x (CReal_opp y).
 
-Infix "-" := CReal_minus : R_scope_constr.
+Infix "-" := CReal_minus : CReal_scope.
 
 Lemma belowMultiple : forall n p : nat, lt 0 p -> le n (p * n).
 Proof.
@@ -1060,6 +1022,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 +1048,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 +1061,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 +1092,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.
@@ -1135,6 +1128,17 @@ Proof.
   - apply CReal_plus_proper_r. apply H.
 Qed.
 
+Instance CReal_plus_morph_T
+  : CMorphisms.Proper
+      (CMorphisms.respectful CRealEq (CMorphisms.respectful CRealEq CRealEq)) CReal_plus.
+Proof.
+  intros x y H z t H0. apply (CRealEq_trans _ (CReal_plus x t)).
+  - destruct H0.
+    split. intro abs. apply CReal_plus_lt_reg_l in abs. contradiction.
+    intro abs. apply CReal_plus_lt_reg_l in abs. contradiction.
+  - apply CReal_plus_proper_r. apply H.
+Qed.
+
 Lemma CReal_plus_eq_reg_l : forall (r r1 r2 : CReal),
     CRealEq (CReal_plus r r1) (CReal_plus r r2)
     -> CRealEq r1 r2.
@@ -1144,7 +1148,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.
@@ -1291,7 +1295,7 @@ Proof.
   apply H; apply linear_max; assumption.
 Defined.
 
-Infix "*" := CReal_mult : R_scope_constr.
+Infix "*" := CReal_mult : CReal_scope.
 
 Lemma CReal_mult_unfold : forall x y : CReal,
     QSeqEquivEx (proj1_sig (CReal_mult x y))
@@ -1451,7 +1455,7 @@ Lemma CReal_mult_lt_0_compat : forall x y : CReal,
     -> CRealLt (inject_Q 0) y
     -> CRealLt (inject_Q 0) (CReal_mult x y).
 Proof.
-  intros. destruct H, H0.
+  intros. destruct H as [x0 H], H0 as [x1 H0].
   pose proof (CRealLt_aboveSig (inject_Q 0) x x0 H).
   pose proof (CRealLt_aboveSig (inject_Q 0) y x1 H0).
   destruct x as [xn limx], y as [yn limy].
@@ -1492,8 +1496,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 +1616,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.
@@ -1692,6 +1704,13 @@ Proof.
   apply CReal_isRingExt.
 Qed.
 
+Instance CReal_mult_morph_T
+  : CMorphisms.Proper
+      (CMorphisms.respectful CRealEq (CMorphisms.respectful CRealEq CRealEq)) CReal_mult.
+Proof.
+  apply CReal_isRingExt.
+Qed.
+
 Add Parametric Morphism : CReal_opp
     with signature CRealEq ==> CRealEq
       as CReal_opp_morph.
@@ -1699,6 +1718,13 @@ Proof.
   apply (Ropp_ext CReal_isRingExt).
 Qed.
 
+Instance CReal_opp_morph_T
+  : CMorphisms.Proper
+      (CMorphisms.respectful CRealEq CRealEq) CReal_opp.
+Proof.
+  apply CReal_isRingExt.
+Qed.
+
 Add Parametric Morphism : CReal_minus
     with signature CRealEq ==> CRealEq ==> CRealEq
       as CReal_minus_morph.
@@ -1706,14 +1732,50 @@ Proof.
   intros. unfold CReal_minus. rewrite H,H0. reflexivity.
 Qed.
 
+Instance CReal_minus_morph_T
+  : CMorphisms.Proper
+      (CMorphisms.respectful CRealEq (CMorphisms.respectful CRealEq CRealEq)) CReal_minus.
+Proof.
+  intros x y exy z t ezt. unfold CReal_minus. rewrite exy,ezt. reflexivity.
+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 +1790,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 +1804,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)
@@ -1753,15 +1820,15 @@ Proof.
   - intro abs. apply (CReal_mult_lt_compat_l (-r)) in abs.
     rewrite <- CReal_opp_mult_distr_l, <- CReal_opp_mult_distr_l, H0 in abs.
     exact (CRealLt_irrefl _ abs). apply (CReal_plus_lt_reg_l r).
-    rewrite CReal_plus_opp_r, CReal_plus_comm, CReal_plus_0_l. exact H.
+    rewrite CReal_plus_opp_r, CReal_plus_comm, CReal_plus_0_l. exact c.
   - intro abs. apply (CReal_mult_lt_compat_l (-r)) in abs.
     rewrite <- CReal_opp_mult_distr_l, <- CReal_opp_mult_distr_l, H0 in abs.
     exact (CRealLt_irrefl _ abs). apply (CReal_plus_lt_reg_l r).
-    rewrite CReal_plus_opp_r, CReal_plus_comm, CReal_plus_0_l. exact H.
+    rewrite CReal_plus_opp_r, CReal_plus_comm, CReal_plus_0_l. exact c.
   - intro abs. apply (CReal_mult_lt_compat_l r) in abs. rewrite H0 in abs.
-    exact (CRealLt_irrefl _ abs). exact H.
+    exact (CRealLt_irrefl _ abs). exact c.
   - intro abs. apply (CReal_mult_lt_compat_l r) in abs. rewrite H0 in abs.
-    exact (CRealLt_irrefl _ abs). exact H.
+    exact (CRealLt_irrefl _ abs). exact c.
 Qed.
 
 
@@ -1783,8 +1850,8 @@ Arguments INR n%nat.
 Fixpoint IPR_2 (p:positive) : CReal :=
   match p with
   | xH => 1 + 1
-  | xO p => (1 + 1) * IPR_2 p
-  | xI p => (1 + 1) * (1 + IPR_2 p)
+  | xO p => IPR_2 p + IPR_2 p
+  | xI p => (1 + IPR_2 p) + (1 + IPR_2 p)
   end.
 
 Definition IPR (p:positive) : CReal :=
@@ -1804,7 +1871,7 @@ Definition IZR (z:Z) : CReal :=
   end.
 Arguments IZR z%Z : simpl never.
 
-Notation "2" := (IZR 2) : R_scope_constr.
+Notation "2" := (IZR 2) : CReal_scope.
 
 (**********)
 Lemma S_INR : forall n:nat, INR (S n) == INR n + 1.
@@ -1812,15 +1879,24 @@ Proof.
   intro; destruct n. rewrite CReal_plus_0_l. reflexivity. reflexivity.
 Qed.
 
+Lemma le_succ_r_T : forall n m : nat, (n <= S m)%nat -> {(n <= m)%nat} + {n = S m}.
+Proof.
+  intros. destruct (le_lt_dec n m). left. exact l.
+  right. apply Nat.le_succ_r in H. destruct H.
+  exfalso. apply (le_not_lt n m); assumption. exact H.
+Qed.
+
 Lemma lt_INR : forall n m:nat, (n < m)%nat -> INR n < INR m.
 Proof.
   induction m.
-  - intros. inversion H.
+  - intros. exfalso. inversion H.
   - intros. unfold lt in H. apply le_S_n in H. destruct m.
-    inversion H. apply CRealLt_0_1. apply Nat.le_succ_r in H. destruct H.
+    assert (n = 0)%nat.
+    { inversion H. reflexivity. }
+    subst n. apply CRealLt_0_1. apply le_succ_r_T in H. destruct H.
     rewrite S_INR. apply (CRealLt_trans _ (INR (S m) + 0)).
     rewrite CReal_plus_comm, CReal_plus_0_l. apply IHm.
-    apply le_n_S. exact H.
+    apply le_n_S. exact l.
     apply CReal_plus_lt_compat_l. exact CRealLt_0_1.
     subst n. rewrite (S_INR (S m)). rewrite <- (CReal_plus_0_l).
     rewrite (CReal_plus_comm 0), CReal_plus_assoc.
@@ -1866,29 +1942,73 @@ Proof.
 Qed.
 
 (**********)
-Lemma IZN : forall n:Z, (0 <= n)%Z ->  exists m : nat, n = Z.of_nat m.
+Lemma IZN : forall n:Z, (0 <= n)%Z -> { m : nat | n = Z.of_nat m }.
 Proof.
-  intros z; idtac; apply Z_of_nat_complete; assumption.
+  intros. exists (Z.to_nat n). rewrite Z2Nat.id. reflexivity. assumption.
 Qed.
 
 Lemma INR_IPR : forall p, INR (Pos.to_nat p) == IPR p.
 Proof.
-  assert (H: forall p, 2 * INR (Pos.to_nat p) == IPR_2 p).
+  assert (H: forall p, INR (Pos.to_nat p) + INR (Pos.to_nat p) == IPR_2 p).
   { induction p as [p|p|].
     - unfold IPR_2; rewrite Pos2Nat.inj_xI, S_INR, mult_INR, <- IHp.
-      rewrite CReal_plus_comm. reflexivity.
-    - unfold IPR_2; now rewrite Pos2Nat.inj_xO, mult_INR, <- IHp.
-    - apply CReal_mult_1_r. }
+      setoid_replace (INR 2) with (1 + 1). 2: reflexivity. ring.
+    - unfold IPR_2; rewrite Pos2Nat.inj_xO, mult_INR, <- IHp.
+      setoid_replace (INR 2) with (1 + 1). 2: reflexivity. ring.
+    - reflexivity. }
   intros [p|p|] ; unfold IPR.
   rewrite Pos2Nat.inj_xI, S_INR, mult_INR, <- H.
-  apply CReal_plus_comm.
-  now rewrite Pos2Nat.inj_xO, mult_INR, <- H.
+  setoid_replace (INR 2) with (1 + 1). 2: reflexivity. ring.
+  rewrite Pos2Nat.inj_xO, mult_INR, <- H.
+  setoid_replace (INR 2) with (1 + 1). 2: reflexivity. ring.
   easy.
 Qed.
 
+(* This is stronger than Req to injectQ, because it
+   concerns all the rational sequence, not only its limit. *)
+Lemma FinjectP2_CReal : forall (p:positive) (k:nat),
+    (proj1_sig (IPR_2 p) k == Z.pos p~0 # 1)%Q.
+Proof.
+  induction p.
+  - intros. replace (IPR_2 p~1) with (1 + IPR_2 p + (1+ IPR_2 p)).
+    2: reflexivity. do 2 rewrite CReal_plus_nth. rewrite IHp.
+    simpl. rewrite Pos2Z.inj_xO, (Pos2Z.inj_xO (p~1)), Pos2Z.inj_xI.
+    generalize (2*Z.pos p)%Z. intro z.
+    do 2 rewrite Qinv_plus_distr. apply f_equal2.
+    2: reflexivity. unfold Qnum. ring.
+  - intros. replace (IPR_2 p~0) with (IPR_2 p + IPR_2 p).
+    2: reflexivity. rewrite CReal_plus_nth, IHp.
+    rewrite Qinv_plus_distr. apply f_equal2. 2: reflexivity.
+    unfold Qnum. rewrite (Pos2Z.inj_xO (p~0)). ring.
+  - intros. reflexivity.
+Qed.
+
+Lemma FinjectP_CReal : forall (p:positive) (k:nat),
+    (proj1_sig (IPR p) k == Z.pos p # 1)%Q.
+Proof.
+  destruct p.
+  - intros. unfold IPR.
+    rewrite CReal_plus_nth, FinjectP2_CReal. unfold Qeq; simpl.
+    rewrite Pos.mul_1_r. reflexivity.
+  - intros. unfold IPR. rewrite FinjectP2_CReal. reflexivity.
+  - intros. reflexivity.
+Qed.
+
+(* Inside this Cauchy real implementation, we can give
+   an instantaneous witness of this inequality, because
+   we know a priori that it will work. *)
 Lemma IPR_pos : forall p:positive, 0 < IPR p.
 Proof.
-  intro p. rewrite <- INR_IPR. apply (lt_INR 0), Pos2Nat.is_pos.
+  intro p. exists 3%positive. simpl.
+  rewrite FinjectP_CReal. apply (Qlt_le_trans _ 1). reflexivity.
+  unfold Qle; simpl.
+  rewrite <- (Zpos_max_1 (p*1*1)). apply Z.le_max_l.
+Defined.
+
+Lemma IPR_double : forall p:positive, IPR (2*p) == 2 * IPR p.
+Proof.
+  intro p.
+  destruct p; rewrite (CReal_mult_plus_distr_r _ 1 1), CReal_mult_1_l; reflexivity.
 Qed.
 
 (**********)
@@ -1939,6 +2059,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).
@@ -1975,7 +2166,7 @@ Qed.
 (* Axiom Rarchimed_constr *)
 Lemma Rarchimedean
   : forall x:CReal,
-    { n:Z | x < IZR n /\ IZR n < x+2 }.
+    { n:Z & x < IZR n < x+2 }.
 Proof.
   (* Locate x within 1/4 and pick the first integer above this interval. *)
   intros [xn limx].
@@ -2018,7 +2209,7 @@ Proof.
 Qed.
 
 Lemma CRealLtDisjunctEpsilon : forall a b c d : CReal,
-    (CRealLt a b \/ CRealLt c d) -> { CRealLt a b } + { CRealLt c d }.
+    (CRealLtProp a b \/ CRealLtProp c d) -> CRealLt a b  +  CRealLt c d.
 Proof.
   intros.
   assert (exists n : nat, n <> O /\
@@ -2100,7 +2291,7 @@ Definition CRealNegShift (x : CReal)
     -> { y : prod positive CReal | CRealEq x (snd y)
                                    /\ forall n:nat, Qlt (proj1_sig (snd y) n) (-1 # fst y) }.
 Proof.
-  intro xNeg. apply CRealLtEpsilon in xNeg.
+  intro xNeg.
   pose proof (CRealLt_aboveSig x (inject_Q 0)).
   pose proof (CRealShiftReal x).
   pose proof (CRealShiftEqual x).
@@ -2137,7 +2328,7 @@ Definition CRealPosShift (x : CReal)
     -> { y : prod positive CReal | CRealEq x (snd y)
                                    /\ forall n:nat, Qlt (1 # fst y) (proj1_sig (snd y) n) }.
 Proof.
-  intro xPos. apply CRealLtEpsilon in xPos.
+  intro xPos.
   pose proof (CRealLt_aboveSig (inject_Q 0) x).
   pose proof (CRealShiftReal x).
   pose proof (CRealShiftEqual x).
@@ -2318,7 +2509,7 @@ Qed.
 
 Definition CReal_inv (x : CReal) (xnz : x # 0) : CReal.
 Proof.
-  apply CRealLtDisjunctEpsilon in xnz. destruct xnz as [xNeg | xPos].
+  destruct xnz as [xNeg | xPos].
   - destruct (CRealNegShift x xNeg) as [[k y] [_ maj]].
     destruct y as [yn cau]; unfold proj1_sig, snd, fst in maj.
     exists (fun n => Qinv (yn (mult (Pos.to_nat k^2) n))).
@@ -2329,17 +2520,17 @@ Proof.
     apply (CReal_inv_pos yn). apply cau. apply maj.
 Defined.
 
-Notation "/ x" := (CReal_inv x) (at level 35, right associativity) : R_scope_constr.
+Notation "/ x" := (CReal_inv x) (at level 35, right associativity) : CReal_scope.
 
 Lemma CReal_inv_0_lt_compat
   : forall (r : CReal) (rnz : r # 0),
     0 < r -> 0 < ((/ r) rnz).
 Proof.
   intros. unfold CReal_inv. simpl.
-  destruct (CRealLtDisjunctEpsilon r (inject_Q 0) (inject_Q 0) r rnz).
+  destruct rnz.
   - exfalso. apply CRealLt_asym in H. contradiction.
   - destruct (CRealPosShift r c) as [[k rpos] [req maj]].
-    clear req. clear rnz. destruct rpos as [rn cau]; simpl in maj.
+    clear req. destruct rpos as [rn cau]; simpl in maj.
     unfold CRealLt; simpl.
     destruct (Qarchimedean (rn 1%nat)) as [A majA].
     exists (2 * (A + 1))%positive. unfold Qminus. rewrite Qplus_0_r.
@@ -2393,7 +2584,7 @@ Lemma CReal_inv_l : forall (r:CReal) (rnz : r # 0),
         ((/ r) rnz) * r == 1.
 Proof.
   intros. unfold CReal_inv; simpl.
-  destruct (CRealLtDisjunctEpsilon r (inject_Q 0) (inject_Q 0) r rnz).
+  destruct rnz.
   - (* r < 0 *) destruct (CRealNegShift r c) as [[k rneg] [req maj]].
     simpl in req. apply CRealEq_diff. apply CRealEq_modindep.
     apply (QSeqEquivEx_trans _
@@ -2478,6 +2669,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) (inr 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
@@ -2488,12 +2745,136 @@ Fixpoint pow (r:CReal) (n:nat) : CReal :=
 (**********)
 Definition IQR (q:Q) : CReal :=
   match q with
-  | Qmake a b => IZR a * (CReal_inv (IPR b)) (or_intror (IPR_pos b))
+  | Qmake a b => IZR a * (CReal_inv (IPR b)) (inr (IPR_pos b))
   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)) (inr (IPR_pos (Qden * Qden0))))
+    with ((/ IPR Qden) (inr (IPR_pos Qden))
+          * (/ IPR Qden0) (inr (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) (inr (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
+                _ _ _ _ (inr (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.
+  apply (CRealLe_trans _ ((/ IPR b) (inr (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.
+  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.
+
+Instance IQR_morph_T
+  : CMorphisms.Proper
+      (CMorphisms.respectful Qeq CRealEq) IQR.
+Proof.
+  intros x y H. destruct x,y; unfold IQR.
+  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)))
+    CRealEq (CReal_inv (inject_Q (Z.pos b # 1)) (inr (CReal_injectQPos (Z.pos b # 1) pos)))
             (inject_Q (1 # b)).
 Proof.
   intros.
@@ -2511,12 +2892,12 @@ Qed.
 Lemma FinjectQ_CReal : forall q : Q,
     IQR q == inject_Q q.
 Proof.
-  intros [a b]. unfold IQR; simpl.
+  intros [a b]. unfold IQR.
   pose proof (CReal_iterate_one (Pos.to_nat b)).
   rewrite positive_nat_Z in H. simpl in H.
   assert (0 < Z.pos b # 1)%Q as pos. reflexivity.
   apply (CRealEq_trans _ (CReal_mult (IZR a)
-                                     (CReal_inv (inject_Q (Z.pos b # 1)) (or_intror (CReal_injectQPos (Z.pos b # 1) pos))))).
+                                     (CReal_inv (inject_Q (Z.pos b # 1)) (inr (CReal_injectQPos (Z.pos b # 1) pos))))).
   - apply CReal_mult_proper_l.
     apply (CReal_mult_eq_reg_l (IPR b)).
     right. apply IPR_pos.
@@ -2530,6 +2911,41 @@ Proof.
     discriminate.
 Qed.
 
-Close Scope R_scope_constr.
+Lemma CReal_gen_inject : forall (n : nat),
+    gen_phiZ (inject_Q 0) (inject_Q 1) CReal_plus CReal_mult CReal_opp
+             (Z.of_nat n)
+    == inject_Q (Z.of_nat n # 1).
+Proof.
+  induction n.
+  - apply CRealEq_refl.
+  - replace (Z.of_nat (S n)) with (1 + Z.of_nat n)%Z.
+    rewrite (gen_phiZ_add CRealEq_rel CReal_isRingExt CReal_isRing).
+    rewrite IHn. clear IHn. apply CRealEq_diff. intro k. simpl.
+    rewrite Z.mul_1_r. rewrite Z.mul_1_r. rewrite Z.mul_1_r.
+    rewrite Z.add_opp_diag_r. discriminate.
+    replace (S n) with (1 + n)%nat. 2: reflexivity.
+    rewrite (Nat2Z.inj_add 1 n). reflexivity.
+Qed.
+
+Lemma CRealArchimedean
+  : forall x:CReal, { n:Z & CRealLt x (gen_phiZ (inject_Q 0) (inject_Q 1) CReal_plus
+                                                CReal_mult CReal_opp n) }.
+Proof.
+  intros [xn limx]. destruct (Qarchimedean (xn 1%nat)) as [k kmaj].
+  exists (Z.pos (2 + k)). rewrite <- (positive_nat_Z (2 + k)).
+  rewrite CReal_gen_inject. rewrite (positive_nat_Z (2 + k)).
+  exists xH.
+  setoid_replace (2 # 1)%Q with
+      ((Z.pos (2 + k) # 1) - (Z.pos k # 1))%Q.
+  - apply Qplus_lt_r. apply Qlt_minus_iff. rewrite Qopp_involutive.
+    apply Qlt_minus_iff in kmaj. rewrite Qplus_comm. apply kmaj.
+  - unfold Qminus. setoid_replace (- (Z.pos k # 1))%Q with (-Z.pos k # 1)%Q.
+    2: reflexivity. rewrite Qinv_plus_distr.
+    rewrite Pos2Z.inj_add. rewrite <- Zplus_assoc.
+    rewrite Zplus_opp_r. reflexivity.
+Qed.
+
+
+Close Scope CReal_scope.
 
 Close Scope Q.
diff --git a/theories/Reals/ConstructiveRIneq.v b/theories/Reals/ConstructiveRIneq.v
index adffa9b719..b53436be55 100644
--- a/theories/Reals/ConstructiveRIneq.v
+++ b/theories/Reals/ConstructiveRIneq.v
@@ -10,68 +10,423 @@
 (************************************************************************)
 
 (*********************************************************)
-(** * Basic lemmas for the classical real numbers        *)
+(** * Basic lemmas for the contructive real numbers      *)
 (*********************************************************)
 
+(* Implement interface ConstructiveReals opaquely with
+   Cauchy reals and prove basic results.
+   Those are therefore true for any implementation of
+   ConstructiveReals (for example with Dedekind reals).
+
+   This file is the recommended import for working with
+   constructive reals, do not use ConstructiveCauchyReals
+   directly. *)
+
 Require Import ConstructiveCauchyReals.
+Require Import ConstructiveRcomplete.
+Require Import ConstructiveRealsLUB.
+Require Export ConstructiveReals.
 Require Import Zpower.
 Require Export ZArithRing.
 Require Import Omega.
 Require Import QArith_base.
 Require Import Qring.
 
+Declare Scope R_scope_constr.
+
 Local Open Scope Z_scope.
 Local Open Scope R_scope_constr.
 
-(* Export all axioms *)
-
-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).
-Notation Rplus_0_l := CReal_plus_0_l (only parsing).
-Notation Rmult_comm := CReal_mult_comm (only parsing).
-Notation Rmult_assoc := CReal_mult_assoc (only parsing).
-Notation Rinv_l := CReal_inv_l (only parsing).
-Notation Rmult_1_l := CReal_mult_1_l (only parsing).
-Notation Rmult_plus_distr_l := CReal_mult_plus_distr_l (only parsing).
-Notation Rlt_0_1 := CRealLt_0_1 (only parsing).
-Notation Rlt_asym := CRealLt_asym (only parsing).
-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).
+Definition CR : ConstructiveReals.
+Proof.
+  assert (isLinearOrder CReal CRealLt) as lin.
+  { repeat split. exact CRealLt_asym.
+    exact CRealLt_trans.
+    intros. destruct (CRealLt_dec x z y H).
+    left. exact c. right. exact c. }
+  apply (Build_ConstructiveReals
+           CReal CRealLt lin CRealLtProp
+           CRealLtEpsilon CRealLtForget CRealLtDisjunctEpsilon
+           (inject_Q 0) (inject_Q 1)
+           CReal_plus CReal_opp CReal_mult
+           CReal_isRing CReal_isRingExt CRealLt_0_1
+           CReal_plus_lt_compat_l CReal_plus_lt_reg_l
+           CReal_mult_lt_0_compat
+           CReal_inv CReal_inv_l CReal_inv_0_lt_compat
+           CRealArchimedean).
+  - intros. destruct (Rcauchy_complete xn) as [l cv].
+    intro n. apply (H (IQR (1#n))). apply IQR_pos. reflexivity.
+    exists l. intros eps epsPos.
+    destruct (Rup_nat ((/eps) (inr epsPos))) as [n nmaj].
+    specialize (cv (Pos.of_nat (S n))) as [p pmaj].
+    exists p. intros. specialize (pmaj i H0). unfold absSmall in pmaj.
+    apply (CReal_mult_lt_compat_l eps) in nmaj.
+    rewrite CReal_inv_r, CReal_mult_comm in nmaj.
+    2: apply epsPos. split.
+    + apply (CRealLt_trans _ (-IQR (1 # Pos.of_nat (S n)))).
+      2: apply pmaj. clear pmaj.
+      apply CReal_opp_gt_lt_contravar. unfold CRealGt, IQR.
+      rewrite CReal_mult_1_l. apply (CReal_mult_lt_reg_l (IPR (Pos.of_nat (S n)))).
+      apply IPR_pos. rewrite CReal_inv_r, <- INR_IPR, Nat2Pos.id.
+      2: discriminate. apply (CRealLt_trans _ (INR n * eps) _ nmaj).
+      apply CReal_mult_lt_compat_r. exact epsPos. apply lt_INR, le_refl.
+    + apply (CRealLt_trans _ (IQR (1 # Pos.of_nat (S n)))).
+      apply pmaj. unfold IQR. rewrite CReal_mult_1_l.
+      apply (CReal_mult_lt_reg_l (IPR (Pos.of_nat (S n)))).
+      apply IPR_pos. rewrite CReal_inv_r, <- INR_IPR, Nat2Pos.id.
+      2: discriminate. apply (CRealLt_trans _ (INR n * eps) _ nmaj).
+      apply CReal_mult_lt_compat_r. exact epsPos. apply lt_INR, le_refl.
+  - exact sig_lub.
+Qed. (* Keep it opaque to possibly change the implementation later *)
+
+Definition R := CRcarrier CR.
+
+Definition Req := orderEq R (CRlt CR).
+Definition Rle (x y : R) := CRlt CR y x -> False.
+Definition Rge (x y : R) := CRlt CR x y -> False.
+Definition Rlt := CRlt CR.
+Definition RltProp := CRltProp CR.
+Definition Rgt (x y : R) := CRlt CR y x.
+Definition Rappart := orderAppart R (CRlt CR).
+
+Infix "==" := Req : R_scope_constr.
+Infix "#" := Rappart : R_scope_constr.
+Infix "<" := Rlt : R_scope_constr.
+Infix ">" := Rgt : R_scope_constr.
+Infix "<=" := Rle : R_scope_constr.
+Infix ">=" := Rge : R_scope_constr.
+
+Notation "x <= y <= z" := (x <= y /\ y <= z) : R_scope_constr.
+Notation "x <= y < z"  := (prod (x <= y) (y < z)) : R_scope_constr.
+Notation "x < y < z"   := (prod (x < y) (y < z)) : R_scope_constr.
+Notation "x < y <= z"  := (prod (x < y) (y <= z)) : R_scope_constr.
+
+Lemma Rlt_epsilon : forall x y : R, RltProp x y -> x < y.
+Proof.
+  exact (CRltEpsilon CR).
+Qed.
+
+Lemma Rlt_forget : forall x y : R, x < y -> RltProp x y.
+Proof.
+  exact (CRltForget CR).
+Qed.
+
+Lemma Rle_refl : forall x : R, x <= x.
+Proof.
+  intros. intro abs.
+  destruct (CRltLinear CR), p.
+  exact (f x x abs abs).
+Qed.
+Hint Immediate Rle_refl: rorders.
+
+Lemma Req_refl : forall x : R, x == x.
+Proof.
+  intros. split; apply Rle_refl.
+Qed.
+
+Lemma Req_sym : forall x y : R, x == y -> y == x.
+Proof.
+  intros. destruct H. split; intro abs; contradiction.
+Qed.
+
+Lemma Req_trans : forall x y z : R, x == y -> y == z -> x == z.
+Proof.
+  intros. destruct H,H0. destruct (CRltLinear CR), p. split.
+  - intro abs. destruct (s _ y _ abs); contradiction.
+  - intro abs. destruct (s _ y _ abs); contradiction.
+Qed.
+
+Add Parametric Relation : R Req
+    reflexivity proved by Req_refl
+    symmetry proved by Req_sym
+    transitivity proved by Req_trans
+      as Req_rel.
+
+Instance Req_relT : CRelationClasses.Equivalence Req.
+Proof.
+  split. exact Req_refl. exact Req_sym. exact Req_trans.
+Qed.
+
+Lemma linear_order_T : forall x y z : R,
+    x < z -> (x < y) + (y < z).
+Proof.
+  intros. destruct (CRltLinear CR). apply s. exact H.
+Qed.
+
+Instance Rlt_morph
+  : CMorphisms.Proper
+      (CMorphisms.respectful Req (CMorphisms.respectful Req CRelationClasses.iffT)) Rlt.
+Proof.
+  intros x y H x0 y0 H0. destruct H, H0. split.
+  - intro. destruct (linear_order_T x y x0). assumption.
+    contradiction. destruct (linear_order_T y y0 x0).
+    assumption. assumption. contradiction.
+  - intro. destruct (linear_order_T y x y0). assumption.
+    contradiction. destruct (linear_order_T x x0 y0).
+    assumption. assumption. contradiction.
+Qed.
+
+Instance RltProp_morph
+  : Morphisms.Proper
+      (Morphisms.respectful Req (Morphisms.respectful Req iff)) RltProp.
+Proof.
+  intros x y H x0 y0 H0. destruct H, H0. split.
+  - intro. destruct (linear_order_T x y x0).
+    apply Rlt_epsilon. assumption.
+    contradiction. destruct (linear_order_T y y0 x0).
+    assumption. apply Rlt_forget. assumption. contradiction.
+  - intro. destruct (linear_order_T y x y0).
+    apply Rlt_epsilon. assumption.
+    contradiction. destruct (linear_order_T x x0 y0).
+    assumption. apply Rlt_forget. assumption. contradiction.
+Qed.
+
+Instance Rgt_morph
+  : CMorphisms.Proper
+      (CMorphisms.respectful Req (CMorphisms.respectful Req CRelationClasses.iffT)) Rgt.
+Proof.
+  intros x y H x0 y0 H0. unfold Rgt. apply Rlt_morph; assumption.
+Qed.
+
+Instance Rappart_morph
+  : CMorphisms.Proper
+      (CMorphisms.respectful Req (CMorphisms.respectful Req CRelationClasses.iffT)) Rappart.
+Proof.
+  split.
+  - intros. destruct H1. left. rewrite <- H0, <- H. exact c.
+    right. rewrite <- H0, <- H. exact c.
+  - intros. destruct H1. left. rewrite H0, H. exact c.
+    right. rewrite H0, H. exact c.
+Qed.
+
+Add Parametric Morphism : Rle
+    with signature Req ==> Req ==> iff
+      as Rle_morph.
+Proof.
+  intros. split.
+  - intros H1 H2. unfold CRealLe in H1.
+    rewrite <- H0 in H2. rewrite <- H in H2. contradiction.
+  - intros H1 H2. unfold CRealLe in H1.
+    rewrite H0 in H2. rewrite H in H2. contradiction.
+Qed.
+
+Add Parametric Morphism : Rge
+    with signature Req ==> Req ==> iff
+      as Rge_morph.
+Proof.
+  intros. unfold Rge. apply Rle_morph; assumption.
+Qed.
+
+
+Definition Rplus := CRplus CR.
+Definition Rmult := CRmult CR.
+Definition Rinv := CRinv CR.
+Definition Ropp := CRopp CR.
+
+Add Parametric Morphism : Rplus
+    with signature Req ==> Req ==> Req
+      as Rplus_morph.
+Proof.
+  apply CRisRingExt.
+Qed.
+
+Instance Rplus_morph_T
+  : CMorphisms.Proper
+      (CMorphisms.respectful Req (CMorphisms.respectful Req Req)) Rplus.
+Proof.
+  apply CRisRingExt.
+Qed.
+
+Add Parametric Morphism : Rmult
+    with signature Req ==> Req ==> Req
+      as Rmult_morph.
+Proof.
+  apply CRisRingExt.
+Qed.
+
+Instance Rmult_morph_T
+  : CMorphisms.Proper
+      (CMorphisms.respectful Req (CMorphisms.respectful Req Req)) Rmult.
+Proof.
+  apply CRisRingExt.
+Qed.
+
+Add Parametric Morphism : Ropp
+    with signature Req ==> Req
+      as Ropp_morph.
+Proof.
+  apply CRisRingExt.
+Qed.
+
+Instance Ropp_morph_T
+  : CMorphisms.Proper
+      (CMorphisms.respectful Req Req) Ropp.
+Proof.
+  apply CRisRingExt.
+Qed.
+
+Infix "+" := Rplus : R_scope_constr.
+Notation "- x" := (Ropp x) : R_scope_constr.
+Definition Rminus (r1 r2:R) : R := r1 + - r2.
+Infix "-" := Rminus : R_scope_constr.
+Infix "*" := Rmult : R_scope_constr.
+Notation "/ x" := (CRinv CR x) (at level 35, right associativity) : R_scope_constr.
+
+Notation "0" := (CRzero CR) : R_scope_constr.
+Notation "1" := (CRone CR) : R_scope_constr.
+
+Add Parametric Morphism : Rminus
+    with signature Req ==> Req ==> Req
+      as Rminus_morph.
+Proof.
+  intros. unfold Rminus, CRminus. rewrite H,H0. reflexivity.
+Qed.
+
+
+(* Help Add Ring to find the correct equality *)
+Lemma RisRing : ring_theory 0 1
+                            Rplus Rmult
+                            Rminus Ropp
+                            Req.
+Proof.
+  exact (CRisRing CR).
+Qed.
+
+Add Ring CRealRing : RisRing.
+
+Lemma Rplus_comm : forall x y:R, x + y == y + x.
+Proof. intros. ring. Qed.
+
+Lemma Rplus_assoc : forall x y z:R, (x + y) + z == x + (y + z).
+Proof. intros. ring. Qed.
+
+Lemma Rplus_opp_r : forall x:R, x + -x == 0.
+Proof. intros. ring. Qed.
+
+Lemma Rplus_0_l : forall x:R, 0 + x == x.
+Proof. intros. ring. Qed.
+
+Lemma Rmult_0_l : forall x:R, 0 * x == 0.
+Proof. intros. ring. Qed.
+
+Lemma Rmult_1_l : forall x:R, 1 * x == x.
+Proof. intros. ring. Qed.
+
+Lemma Rmult_comm : forall x y:R, x * y == y * x.
+Proof. intros. ring. Qed.
+
+Lemma Rmult_assoc : forall x y z:R, (x * y) * z == x * (y * z).
+Proof. intros. ring. Qed.
+
+Definition Rinv_l := CRinv_l CR.
+
+Lemma Rmult_plus_distr_l : forall r1 r2 r3 : R,
+    r1 * (r2 + r3) == (r1 * r2) + (r1 * r3).
+Proof. intros. ring. Qed.
+
+Definition Rlt_0_1 := CRzero_lt_one CR.
+
+Lemma Rlt_asym : forall x y :R, x < y -> y < x -> False.
+Proof.
+  intros. destruct (CRltLinear CR), p.
+  apply (f x y); assumption.
+Qed.
+
+Lemma Rlt_trans : forall x y z : R, x < y -> y < z -> x < z.
+Proof.
+  intros. destruct (CRltLinear CR), p.
+  apply (c x y); assumption.
+Qed.
+
+Lemma Rplus_lt_compat_l : forall x y z : R,
+    y < z -> x + y < x + z.
+Proof.
+  intros. apply CRplus_lt_compat_l. exact H.
+Qed.
+
+Lemma Ropp_mult_distr_l
+  : forall r1 r2 : R, -(r1 * r2) == (- r1) * r2.
+Proof.
+  intros. ring.
+Qed.
+
+Lemma Rplus_lt_reg_l : forall r r1 r2, r + r1 < r + r2 -> r1 < r2.
+Proof.
+  intros. apply CRplus_lt_reg_l in H. exact H.
+Qed.
+
+Lemma Rmult_lt_compat_l : forall x y z : R,
+    0 < x -> y < z -> x * y < x * z.
+Proof.
+  intros. apply (CRplus_lt_reg_l CR (- (x * y))).
+  rewrite Rplus_comm. pose proof Rplus_opp_r.
+  rewrite H1.
+  rewrite Rmult_comm, Ropp_mult_distr_l, Rmult_comm.
+  rewrite <- Rmult_plus_distr_l.
+  apply CRmult_lt_0_compat. exact H.
+  apply (Rplus_lt_reg_l y).
+  rewrite Rplus_comm, Rplus_0_l.
+  rewrite <- Rplus_assoc, H1, Rplus_0_l. exact H0.
+Qed.
 
 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.
 
+Fixpoint INR (n:nat) : R :=
+  match n with
+  | O => 0
+  | S O => 1
+  | S n => INR n + 1
+  end.
+Arguments INR n%nat.
+
+(* compact representation for 2*p *)
+Fixpoint IPR_2 (p:positive) : R :=
+  match p with
+  | xH => 1 + 1
+  | xO p => (1 + 1) * IPR_2 p
+  | xI p => (1 + 1) * (1 + IPR_2 p)
+  end.
+
+Definition IPR (p:positive) : R :=
+  match p with
+  | xH => 1
+  | xO p => IPR_2 p
+  | xI p => 1 + IPR_2 p
+  end.
+Arguments IPR p%positive : simpl never.
+
+(**********)
+Definition IZR (z:Z) : R :=
+  match z with
+  | Z0 => 0
+  | Zpos n => IPR n
+  | Zneg n => - IPR n
+  end.
+Arguments IZR z%Z : simpl never.
+
+Notation "2" := (IZR 2) : R_scope_constr.
+
 
 (*********************************************************)
 (** ** Relation between orders and equality              *)
 (*********************************************************)
 
-(** Reflexivity of the large order *)
-
-Lemma Rle_refl : forall r, r <= r.
-Proof.
-  intros r abs. apply (CRealLt_asym r r); exact abs.
-Qed.
-Hint Immediate Rle_refl: rorders.
-
 Lemma Rge_refl : forall r, r <= r.
 Proof. exact Rle_refl. Qed.
 Hint Immediate Rge_refl: rorders.
 
 (** Irreflexivity of the strict order *)
 
-Lemma Rlt_irrefl : forall r, ~ r < r.
+Lemma Rlt_irrefl : forall r, r < r -> False.
 Proof.
-  intros r H; eapply CRealLt_asym; eauto.
+  intros r H; eapply Rlt_asym; eauto.
 Qed.
 Hint Resolve Rlt_irrefl: creal.
 
-Lemma Rgt_irrefl : forall r, ~ r > r.
+Lemma Rgt_irrefl : forall r, r > r -> False.
 Proof. exact Rlt_irrefl. Qed.
 
 Lemma Rlt_not_eq : forall r1 r2, r1 < r2 -> r1 <> r2.
@@ -85,11 +440,11 @@ Proof.
 Qed.
 
 (**********)
-Lemma Rlt_dichotomy_converse : forall r1 r2, r1 < r2 \/ r1 > r2 -> r1 <> r2.
+Lemma Rlt_dichotomy_converse : forall r1 r2, ((r1 < r2) + (r1 > r2)) -> r1 <> r2.
 Proof.
   intros. destruct H.
-  - intro abs. subst r2. exact (Rlt_irrefl r1 H).
-  - intro abs. subst r2. exact (Rlt_irrefl r1 H).
+  - intro abs. subst r2. exact (Rlt_irrefl r1 r).
+  - intro abs. subst r2. exact (Rlt_irrefl r1 r).
 Qed.
 Hint Resolve Rlt_dichotomy_converse: creal.
 
@@ -108,13 +463,13 @@ Hint Resolve Rlt_dichotomy_converse: creal.
 
 Lemma Rlt_le : forall r1 r2, r1 < r2 -> r1 <= r2.
 Proof.
-  intros. intro abs. apply (CRealLt_asym r1 r2); assumption.
+  intros. intro abs. apply (Rlt_asym r1 r2); assumption.
 Qed.
 Hint Resolve Rlt_le: creal.
 
 Lemma Rgt_ge : forall r1 r2, r1 > r2 -> r1 >= r2.
 Proof.
-  intros. intro abs. apply (CRealLt_asym r1 r2); assumption.
+  intros. intro abs. apply (Rlt_asym r1 r2); assumption.
 Qed.
 
 (**********)
@@ -147,22 +502,22 @@ Hint Immediate Rgt_lt: rorders.
 
 (**********)
 
-Lemma Rnot_lt_le : forall r1 r2, ~ r1 < r2 -> r2 <= r1.
+Lemma Rnot_lt_le : forall r1 r2, (r1 < r2 -> False) -> r2 <= r1.
 Proof.
-  intros. intro abs. contradiction.
+  intros. exact H.
 Qed.
 
-Lemma Rnot_gt_le : forall r1 r2, ~ r1 > r2 -> r1 <= r2.
+Lemma Rnot_gt_le : forall r1 r2, (r1 > r2 -> False) -> r1 <= r2.
 Proof.
   intros. intro abs. contradiction.
 Qed.
 
-Lemma Rnot_gt_ge : forall r1 r2, ~ r1 > r2 -> r2 >= r1.
+Lemma Rnot_gt_ge : forall r1 r2, (r1 > r2 -> False) -> r2 >= r1.
 Proof.
   intros. intro abs. contradiction.
 Qed.
 
-Lemma Rnot_lt_ge : forall r1 r2, ~ r1 < r2 -> r1 >= r2.
+Lemma Rnot_lt_ge : forall r1 r2, (r1 < r2 -> False) -> r1 >= r2.
 Proof.
   intros. intro abs. contradiction.
 Qed.
@@ -170,7 +525,7 @@ Qed.
 (**********)
 Lemma Rlt_not_le : forall r1 r2, r2 < r1 -> ~ r1 <= r2.
 Proof.
-  generalize CRealLt_asym Rlt_dichotomy_converse; unfold CRealLe.
+  generalize Rlt_asym Rlt_dichotomy_converse; unfold CRealLe.
   unfold not; intuition eauto 3.
 Qed.
 Hint Immediate Rlt_not_le: creal.
@@ -185,19 +540,19 @@ Hint Immediate Rlt_not_ge: creal.
 Lemma Rgt_not_ge : forall r1 r2, r2 > r1 -> ~ r1 >= r2.
 Proof. exact Rlt_not_ge. Qed.
 
-Lemma Rle_not_lt : forall r1 r2, r2 <= r1 -> ~ r1 < r2.
+Lemma Rle_not_lt : forall r1 r2, r2 <= r1 -> r1 < r2 -> False.
 Proof.
-  intros r1 r2. generalize (CRealLt_asym r1 r2) (Rlt_dichotomy_converse r1 r2).
+  intros r1 r2. generalize (Rlt_asym r1 r2) (Rlt_dichotomy_converse r1 r2).
   unfold CRealLe; intuition.
 Qed.
 
-Lemma Rge_not_lt : forall r1 r2, r1 >= r2 -> ~ r1 < r2.
-Proof. intros; apply Rle_not_lt; auto with creal. Qed.
+Lemma Rge_not_lt : forall r1 r2, r1 >= r2 -> r1 < r2 -> False.
+Proof. intros; apply (Rle_not_lt r1 r2); auto with creal. Qed.
 
-Lemma Rle_not_gt : forall r1 r2, r1 <= r2 -> ~ r1 > r2.
+Lemma Rle_not_gt : forall r1 r2, r1 <= r2 -> r1 > r2 -> False.
 Proof. do 2 intro; apply Rle_not_lt. Qed.
 
-Lemma Rge_not_gt : forall r1 r2, r2 >= r1 -> ~ r1 > r2.
+Lemma Rge_not_gt : forall r1 r2, r2 >= r1 -> r1 > r2 -> False.
 Proof. do 2 intro; apply Rge_not_lt. Qed.
 
 (**********)
@@ -227,10 +582,10 @@ Hint Immediate Req_ge_sym: creal.
 
 (** *** Asymmetry *)
 
-(** Remark: [CRealLt_asym] is an axiom *)
+(** Remark: [Rlt_asym] is an axiom *)
 
-Lemma Rgt_asym : forall r1 r2, r1 > r2 -> ~ r2 > r1.
-Proof. do 2 intro; apply CRealLt_asym. Qed.
+Lemma Rgt_asym : forall r1 r2, r1 > r2 -> r2 > r1 -> False.
+Proof. do 2 intro; apply Rlt_asym. Qed.
 
 
 (** *** Compatibility with equality *)
@@ -260,20 +615,20 @@ Qed.
 
 Lemma Rgt_trans : forall r1 r2 r3, r1 > r2 -> r2 > r3 -> r1 > r3.
 Proof.
-  intros. apply (CRealLt_trans _ r2); assumption.
+  intros. apply (Rlt_trans _ r2); assumption.
 Qed.
 
 (**********)
 Lemma Rle_lt_trans : forall r1 r2 r3, r1 <= r2 -> r2 < r3 -> r1 < r3.
 Proof.
   intros.
-  destruct (linear_order_T r2 r1 r3 H0). contradiction. apply c.
+  destruct (linear_order_T r2 r1 r3 H0). contradiction. apply r.
 Qed.
 
 Lemma Rlt_le_trans : forall r1 r2 r3, r1 < r2 -> r2 <= r3 -> r1 < r3.
 Proof.
   intros.
-  destruct (linear_order_T r1 r3 r2 H). apply c. contradiction.
+  destruct (linear_order_T r1 r3 r2 H). apply r. contradiction.
 Qed.
 
 Lemma Rge_gt_trans : forall r1 r2 r3, r1 >= r2 -> r2 > r3 -> r1 > r3.
@@ -367,7 +722,7 @@ Qed.
 Lemma Rinv_r : forall r (rnz : r # 0),
     r # 0 -> r * ((/ r) rnz) == 1.
 Proof.
-  intros. rewrite Rmult_comm. rewrite CReal_inv_l.
+  intros. rewrite Rmult_comm. rewrite Rinv_l.
   reflexivity.
 Qed.
 Hint Resolve Rinv_r: creal.
@@ -455,17 +810,17 @@ Qed.
 
 (**********)
 Lemma Rmult_integral_contrapositive :
-  forall r1 r2, r1 # 0 /\ r2 # 0 -> (r1 * r2) # 0.
+  forall r1 r2, (prod (r1 # 0) (r2 # 0)) -> (r1 * r2) # 0.
 Proof.
   assert (forall r, 0 > r -> 0 < - r).
   { intros. rewrite <- (Rplus_opp_l r), <- (Rplus_0_r (-r)), Rplus_assoc.
     apply Rplus_lt_compat_l. rewrite Rplus_0_l. apply H. }
-  intros. destruct H0, H0, H1.
+  intros. destruct H0, r, r0.
   - right. setoid_replace (r1*r2) with (-r1 * -r2). 2: ring.
     rewrite <- (Rmult_0_r (-r1)). apply Rmult_lt_compat_l; apply H; assumption.
   - left. rewrite <- (Rmult_0_r r2).
-    rewrite Rmult_comm. apply (Rmult_lt_compat_l). apply H1. apply H0.
-  - left. rewrite <- (Rmult_0_r r1). apply (Rmult_lt_compat_l). apply H0. apply H1.
+    rewrite Rmult_comm. apply (Rmult_lt_compat_l). apply c0. apply c.
+  - left. rewrite <- (Rmult_0_r r1). apply (Rmult_lt_compat_l). apply c. apply c0.
   - right. rewrite <- (Rmult_0_r r1). apply Rmult_lt_compat_l; assumption.
 Qed.
 Hint Resolve Rmult_integral_contrapositive: creal.
@@ -489,7 +844,7 @@ Qed.
 (*********************************************************)
 
 (***********)
-Definition Rsqr (r : CReal) := r * r.
+Definition Rsqr (r : R) := r * r.
 
 Notation "r ²" := (Rsqr r) (at level 1, format "r ²") : R_scope_constr.
 
@@ -541,11 +896,6 @@ Hint Resolve Ropp_plus_distr: creal.
 (** ** Opposite and multiplication                       *)
 (*********************************************************)
 
-Lemma Ropp_mult_distr_l : forall r1 r2, - (r1 * r2) == - r1 * r2.
-Proof.
-  intros; ring.
-Qed.
-
 Lemma Ropp_mult_distr_l_reverse : forall r1 r2, - r1 * r2 == - (r1 * r2).
 Proof.
   intros; ring.
@@ -575,13 +925,13 @@ Qed.
 
 Lemma Rminus_0_r : forall r, r - 0 == r.
 Proof.
-  intro; ring.
+  intro r. unfold Rminus. ring.
 Qed.
 Hint Resolve Rminus_0_r: creal.
 
 Lemma Rminus_0_l : forall r, 0 - r == - r.
 Proof.
-  intro; ring.
+  intro r. unfold Rminus. ring.
 Qed.
 Hint Resolve Rminus_0_l: creal.
 
@@ -600,22 +950,22 @@ Qed.
 (**********)
 Lemma Rminus_diag_eq : forall r1 r2, r1 == r2 -> r1 - r2 == 0.
 Proof.
-  intros; rewrite H; ring.
+  intros; rewrite H; unfold Rminus; ring.
 Qed.
 Hint Resolve Rminus_diag_eq: creal.
 
 (**********)
 Lemma Rminus_diag_uniq : forall r1 r2, r1 - r2 == 0 -> r1 == r2.
 Proof.
-  intros r1 r2. unfold CReal_minus; rewrite Rplus_comm; intro.
+  intros r1 r2. unfold Rminus,CRminus; rewrite Rplus_comm; intro.
   rewrite <- (Ropp_involutive r2); apply (Rplus_opp_r_uniq (- r2) r1 H).
 Qed.
 Hint Immediate Rminus_diag_uniq: creal.
 
 Lemma Rminus_diag_uniq_sym : forall r1 r2, r2 - r1 == 0 -> r1 == r2.
 Proof.
-  intros; generalize (Rminus_diag_uniq r2 r1 H); clear H; intro H; rewrite H;
-    ring.
+  intros; generalize (Rminus_diag_uniq r2 r1 H); clear H;
+    intro H; rewrite H; reflexivity.
 Qed.
 Hint Immediate Rminus_diag_uniq_sym: creal.
 
@@ -661,11 +1011,6 @@ Proof. do 3 intro; apply Rplus_lt_compat_r. Qed.
 
 (**********)
 
-Lemma Rplus_lt_reg_l : forall r r1 r2, r + r1 < r + r2 -> r1 < r2.
-Proof.
-  intros. apply CReal_plus_lt_reg_l in H. exact H.
-Qed.
-
 Lemma Rplus_lt_reg_r : forall r r1 r2, r1 + r < r2 + r -> r1 < r2.
 Proof.
   intros.
@@ -701,7 +1046,7 @@ Qed.
 Lemma Rplus_lt_compat :
   forall r1 r2 r3 r4, r1 < r2 -> r3 < r4 -> r1 + r3 < r2 + r4.
 Proof.
-  intros; apply CRealLt_trans with (r2 + r3); auto with creal.
+  intros; apply Rlt_trans with (r2 + r3); auto with creal.
 Qed.
 Hint Immediate Rplus_lt_compat: creal.
 
@@ -754,7 +1099,7 @@ Qed.
 (**********)
 Lemma Rplus_lt_0_compat : forall r1 r2, 0 < r1 -> 0 < r2 -> 0 < r1 + r2.
 Proof.
-  intros. apply (CRealLt_trans _ (r1+0)). rewrite Rplus_0_r. exact H.
+  intros. apply (Rlt_trans _ (r1+0)). rewrite Rplus_0_r. exact H.
   apply Rplus_lt_compat_l. exact H0.
 Qed.
 
@@ -882,11 +1227,11 @@ Proof.
   setoid_replace (r2 + r1 + - r2) with r1 by ring.
   exact H.
 Qed.
-Hint Resolve Ropp_gt_lt_contravar : core.
+Hint Resolve Ropp_gt_lt_contravar : creal.
 
 Lemma Ropp_lt_gt_contravar : forall r1 r2, r1 < r2 -> - r1 > - r2.
 Proof.
-  unfold CRealGt; auto with creal.
+  intros. apply Ropp_gt_lt_contravar. exact H.
 Qed.
 Hint Resolve Ropp_lt_gt_contravar: creal.
 
@@ -942,13 +1287,13 @@ Qed.
 (**********)
 Lemma Ropp_0_lt_gt_contravar : forall r, 0 < r -> 0 > - r.
 Proof.
-  intros; setoid_replace 0 with (-0); auto with creal.
+  intros; setoid_replace 0 with (-0); auto with creal. ring.
 Qed.
 Hint Resolve Ropp_0_lt_gt_contravar: creal.
 
 Lemma Ropp_0_gt_lt_contravar : forall r, 0 > r -> 0 < - r.
 Proof.
-  intros; setoid_replace 0 with (-0); auto with creal.
+  intros; setoid_replace 0 with (-0); auto with creal. ring.
 Qed.
 Hint Resolve Ropp_0_gt_lt_contravar: creal.
 
@@ -968,13 +1313,13 @@ Hint Resolve Ropp_gt_lt_0_contravar: creal.
 (**********)
 Lemma Ropp_0_le_ge_contravar : forall r, 0 <= r -> 0 >= - r.
 Proof.
-  intros; setoid_replace 0 with (-0); auto with creal.
+  intros; setoid_replace 0 with (-0); auto with creal. ring.
 Qed.
 Hint Resolve Ropp_0_le_ge_contravar: creal.
 
 Lemma Ropp_0_ge_le_contravar : forall r, 0 >= r -> 0 <= - r.
 Proof.
-  intros; setoid_replace 0 with (-0); auto with creal.
+  intros; setoid_replace 0 with (-0); auto with creal. ring.
 Qed.
 Hint Resolve Ropp_0_ge_le_contravar: creal.
 
@@ -1019,7 +1364,7 @@ Lemma Rmult_gt_0_lt_compat :
   forall r1 r2 r3 r4,
     r3 > 0 -> r2 > 0 -> r1 < r2 -> r3 < r4 -> r1 * r3 < r2 * r4.
 Proof.
-  intros; apply CRealLt_trans with (r2 * r3); auto with creal.
+  intros; apply Rlt_trans with (r2 * r3); auto with creal.
 Qed.
 
 (*********)
@@ -1048,15 +1393,15 @@ Qed.
 
 (** *** Cancellation *)
 
-Lemma Rinv_0_lt_compat : forall r (rpos : 0 < r), 0 < (/ r) (or_intror rpos).
+Lemma Rinv_0_lt_compat : forall r (rpos : 0 < r), 0 < (/ r) (inr rpos).
 Proof.
-  intros. apply CReal_inv_0_lt_compat. exact rpos.
+  intros. apply CRinv_0_lt_compat. exact rpos.
 Qed.
 
 Lemma Rmult_lt_reg_l : forall r r1 r2, 0 < r -> r * r1 < r * r2 -> r1 < r2.
 Proof.
   intros z x y H H0.
-  apply (Rmult_lt_compat_l ((/z) (or_intror H))) in H0.
+  apply (Rmult_lt_compat_l ((/z) (inr H))) in H0.
   repeat rewrite <- Rmult_assoc in H0. rewrite Rinv_l in H0.
   repeat rewrite Rmult_1_l in H0. apply H0.
   apply Rinv_0_lt_compat.
@@ -1117,13 +1462,17 @@ Qed.
 Lemma Rle_minus : forall r1 r2, r1 <= r2 -> r1 - r2 <= 0.
 Proof.
   intros. intro abs. apply (Rplus_lt_compat_l r2) in abs.
-  ring_simplify in abs. contradiction.
+  unfold Rminus in abs.
+  rewrite Rplus_0_r, Rplus_comm, Rplus_assoc, Rplus_opp_l, Rplus_0_r in abs.
+  contradiction.
 Qed.
 
 Lemma Rge_minus : forall r1 r2, r1 >= r2 -> r1 - r2 >= 0.
 Proof.
   intros. intro abs. apply (Rplus_lt_compat_l r2) in abs.
-  ring_simplify in abs. contradiction.
+  unfold Rminus in abs.
+  rewrite Rplus_0_r, Rplus_comm, Rplus_assoc, Rplus_opp_l, Rplus_0_r in abs.
+  contradiction.
 Qed.
 
 (**********)
@@ -1159,7 +1508,7 @@ Qed.
 Lemma tech_Rplus : forall r s, 0 <= r -> 0 < s -> r + s <> 0.
 Proof.
   intros; apply not_eq_sym; apply Rlt_not_eq.
-  rewrite Rplus_comm; setoid_replace 0 with (0 + 0); auto with creal.
+  rewrite Rplus_comm; setoid_replace 0 with (0 + 0); auto with creal. ring.
 Qed.
 Hint Immediate tech_Rplus: creal.
 
@@ -1169,7 +1518,7 @@ Hint Immediate tech_Rplus: creal.
 
 Lemma Rle_0_1 : 0 <= 1.
 Proof.
-  intro abs. apply (CRealLt_asym 0 1).
+  intro abs. apply (Rlt_asym 0 1).
   apply Rlt_0_1. apply abs.
 Qed.
 
@@ -1200,9 +1549,9 @@ Qed.
 Lemma Rinv_neq_0_compat : forall r (rnz : r # 0), ((/ r) rnz) # 0.
 Proof.
   intros. destruct rnz. left.
-  assert (0 < (/-r) (or_intror (Ropp_0_gt_lt_contravar _ c))).
+  assert (0 < (/-r) (inr (Ropp_0_gt_lt_contravar _ c))).
   { apply Rinv_0_lt_compat. }
-  rewrite <- (Ropp_inv_permute _ (or_introl c)) in H.
+  rewrite <- (Ropp_inv_permute _ (inl c)) in H.
   apply Ropp_lt_cancel. rewrite Ropp_0. exact H.
   right. apply Rinv_0_lt_compat.
 Qed.
@@ -1275,9 +1624,9 @@ Qed.
 (** ** Order and inverse                                 *)
 (*********************************************************)
 
-Lemma Rinv_lt_0_compat : forall r (rneg : r < 0), (/ r) (or_introl rneg) < 0.
+Lemma Rinv_lt_0_compat : forall r (rneg : r < 0), (/ r) (inl rneg) < 0.
 Proof.
-  intros. assert (0 < (/-r) (or_intror (Ropp_0_gt_lt_contravar r rneg))).
+  intros. assert (0 < (/-r) (inr (Ropp_0_gt_lt_contravar r rneg))).
   { apply Rinv_0_lt_compat. }
   rewrite <- Ropp_inv_permute in H. rewrite <- Ropp_0 in H.
   apply Ropp_lt_cancel in H. apply H.
@@ -1310,7 +1659,7 @@ Hint Resolve Rlt_plus_1: creal.
 Lemma tech_Rgt_minus : forall r1 r2, 0 < r2 -> r1 > r1 - r2.
 Proof.
   intros. apply (Rplus_lt_reg_r r2).
-  unfold CReal_minus; rewrite Rplus_assoc, Rplus_opp_l.
+  unfold Rminus, CRminus; rewrite Rplus_assoc, Rplus_opp_l.
   apply Rplus_lt_compat_l. exact H.
 Qed.
 
@@ -1318,7 +1667,89 @@ Qed.
 (** ** Injection from [N] to [R]                         *)
 (*********************************************************)
 
-Lemma Rpow_eq_compat : forall (x y : CReal) (n : nat),
+(**********)
+Lemma S_INR : forall n:nat, INR (S n) == INR n + 1.
+Proof.
+  intro; destruct n. rewrite Rplus_0_l. reflexivity. reflexivity.
+Qed.
+
+Lemma lt_INR : forall n m:nat, (n < m)%nat -> INR n < INR m.
+Proof.
+  induction m.
+  - intros. exfalso. inversion H.
+  - intros. unfold lt in H. apply le_S_n in H. destruct m.
+    assert (n = 0)%nat.
+    { inversion H. reflexivity. }
+    subst n. apply Rlt_0_1. apply le_succ_r_T in H. destruct H.
+    rewrite S_INR. apply (Rlt_trans _ (INR (S m) + 0)).
+    rewrite Rplus_comm, Rplus_0_l. apply IHm.
+    apply le_n_S. exact l.
+    apply Rplus_lt_compat_l. exact Rlt_0_1.
+    subst n. rewrite (S_INR (S m)). rewrite <- (Rplus_0_l).
+    rewrite (Rplus_comm 0), Rplus_assoc.
+    apply Rplus_lt_compat_l. rewrite Rplus_0_l.
+    exact Rlt_0_1.
+Qed.
+
+(**********)
+Lemma S_O_plus_INR : forall n:nat, INR (1 + n) == INR 1 + INR n.
+Proof.
+  intros; destruct n.
+  - rewrite Rplus_comm, Rplus_0_l. reflexivity.
+  - rewrite Rplus_comm. reflexivity.
+Qed.
+
+(**********)
+Lemma plus_INR : forall n m:nat, INR (n + m) == INR n + INR m.
+Proof.
+  intros n m; induction  n as [| n Hrecn].
+  - rewrite Rplus_0_l. reflexivity.
+  - replace (S n + m)%nat with (S (n + m)); auto with arith.
+    repeat rewrite S_INR.
+    rewrite Hrecn; ring.
+Qed.
+
+(**********)
+Lemma minus_INR : forall n m:nat, (m <= n)%nat -> INR (n - m) == INR n - INR m.
+Proof.
+  intros n m le; pattern m, n; apply le_elim_rel.
+  intros. rewrite <- minus_n_O. simpl.
+  unfold Rminus, CRminus. rewrite Ropp_0, Rplus_0_r. reflexivity.
+  intros; repeat rewrite S_INR; simpl.
+  rewrite H0. unfold Rminus. ring. exact le.
+Qed.
+
+(*********)
+Lemma mult_INR : forall n m:nat, INR (n * m) == INR n * INR m.
+Proof.
+  intros n m; induction  n as [| n Hrecn].
+  - rewrite Rmult_0_l. reflexivity.
+  - intros; repeat rewrite S_INR; simpl.
+    rewrite plus_INR. rewrite Hrecn; ring.
+Qed.
+
+Lemma INR_IPR : forall p, INR (Pos.to_nat p) == IPR p.
+Proof.
+  assert (H: forall p, 2 * INR (Pos.to_nat p) == IPR_2 p).
+  { induction p as [p|p|].
+    - unfold IPR_2; rewrite Pos2Nat.inj_xI, S_INR, mult_INR, <- IHp.
+      rewrite Rplus_comm. reflexivity.
+    - unfold IPR_2; now rewrite Pos2Nat.inj_xO, mult_INR, <- IHp.
+    - apply Rmult_1_r. }
+  intros [p|p|] ; unfold IPR.
+  rewrite Pos2Nat.inj_xI, S_INR, mult_INR, <- H.
+  apply Rplus_comm.
+  now rewrite Pos2Nat.inj_xO, mult_INR, <- H.
+  easy.
+Qed.
+
+Fixpoint pow (r:R) (n:nat) : R :=
+  match n with
+    | O => 1
+    | S n => r * (pow r n)
+  end.
+
+Lemma Rpow_eq_compat : forall (x y : R) (n : nat),
     x == y -> pow x n == pow y n.
 Proof.
   intro x. induction n.
@@ -1332,17 +1763,10 @@ Proof. now induction n as [|n IHn];[ | simpl; rewrite mult_INR, IHn]. Qed.
 (*********)
 Lemma lt_0_INR : forall n:nat, (0 < n)%nat -> 0 < INR n.
 Proof.
-  simple induction 1; intros. apply Rlt_0_1.
-  rewrite S_INR. apply (CRealLt_trans _ (INR m)). apply H1. apply Rlt_plus_1.
+  intros. apply (lt_INR 0). exact H.
 Qed.
 Hint Resolve lt_0_INR: creal.
 
-Notation lt_INR := lt_INR (only parsing).
-Notation plus_INR := plus_INR (only parsing).
-Notation INR_IPR := INR_IPR (only parsing).
-Notation plus_IZR_NEG_POS := plus_IZR_NEG_POS (only parsing).
-Notation plus_IZR := plus_IZR (only parsing).
-
 Lemma lt_1_INR : forall n:nat, (1 < n)%nat -> 1 < INR n.
 Proof.
   apply lt_INR.
@@ -1413,9 +1837,10 @@ Hint Resolve not_0_INR: creal.
 
 Lemma not_INR : forall n m:nat, n <> m -> INR n # INR m.
 Proof.
-  intros n m H; case (le_or_lt n m); intros H1.
+  intros n m H; case (le_lt_dec n m); intros H1.
+  left. apply lt_INR.
   case (le_lt_or_eq _ _ H1); intros H2.
-  left. apply lt_INR. exact H2. contradiction.
+  exact H2. contradiction.
   right. apply lt_INR. exact H1.
 Qed.
 Hint Resolve not_INR: creal.
@@ -1456,6 +1881,64 @@ Hint Resolve not_1_INR: creal.
 (** ** Injection from [Z] to [R]                         *)
 (*********************************************************)
 
+Lemma IPR_pos : forall p:positive, 0 < IPR p.
+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 Rmult_1_r. reflexivity.
+Qed.
+
+Lemma INR_IZR_INZ : forall n:nat, INR n == IZR (Z.of_nat n).
+Proof.
+  intros [|n].
+  easy.
+  simpl Z.of_nat. unfold IZR.
+  now rewrite <- INR_IPR, SuccNat2Pos.id_succ.
+Qed.
+
+Lemma plus_IZR_NEG_POS :
+  forall p q:positive, IZR (Zpos p + Zneg q) == IZR (Zpos p) + IZR (Zneg q).
+Proof.
+  intros p q; simpl. rewrite Z.pos_sub_spec.
+  case Pos.compare_spec; intros H; unfold IZR.
+  subst. ring.
+  rewrite <- 3!INR_IPR, Pos2Nat.inj_sub.
+  rewrite minus_INR.
+  2: (now apply lt_le_weak, Pos2Nat.inj_lt).
+  ring.
+  trivial.
+  rewrite <- 3!INR_IPR, Pos2Nat.inj_sub.
+  rewrite minus_INR.
+  2: (now apply lt_le_weak, Pos2Nat.inj_lt).
+  unfold Rminus. ring. trivial.
+Qed.
+
+Lemma plus_IPR : forall n m:positive, IPR (n + m) == IPR n + IPR m.
+Proof.
+  intros. repeat rewrite <- INR_IPR.
+  rewrite Pos2Nat.inj_add. apply plus_INR.
+Qed.
+
+(**********)
+Lemma plus_IZR : forall n m:Z, IZR (n + m) == IZR n + IZR m.
+Proof.
+  intro z; destruct z; intro t; destruct t; intros.
+  - rewrite Rplus_0_l. reflexivity.
+  - rewrite Rplus_0_l. rewrite Z.add_0_l. reflexivity.
+  - rewrite Rplus_0_l. reflexivity.
+  - rewrite Rplus_comm,Rplus_0_l. reflexivity.
+  - rewrite <- Pos2Z.inj_add. unfold IZR. apply plus_IPR.
+  - apply plus_IZR_NEG_POS.
+  - rewrite Rplus_comm,Rplus_0_l, Z.add_0_r. reflexivity.
+  - rewrite Z.add_comm; rewrite Rplus_comm; apply plus_IZR_NEG_POS.
+  - simpl. unfold IZR. rewrite <- 3!INR_IPR, Pos2Nat.inj_add, plus_INR.
+    ring.
+Qed.
+
 Lemma mult_IPR : forall n m:positive, IPR (n * m) == IPR n * IPR m.
 Proof.
   intros. repeat rewrite <- INR_IPR.
@@ -1495,6 +1978,7 @@ Qed.
 Lemma opp_IZR : forall n:Z, IZR (- n) == - IZR n.
 Proof.
   intros [|z|z]; unfold IZR; simpl; auto with creal.
+  ring.
   reflexivity. rewrite Ropp_involutive. reflexivity.
 Qed.
 
@@ -1502,7 +1986,7 @@ Definition Ropp_Ropp_IZR := opp_IZR.
 
 Lemma minus_IZR : forall n m:Z, IZR (n - m) == IZR n - IZR m.
 Proof.
-  intros; unfold Z.sub, CReal_minus.
+  intros; unfold Z.sub, Rminus,CRminus.
   rewrite <- opp_IZR.
   apply plus_IZR.
 Qed.
@@ -1510,8 +1994,8 @@ 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 <- (Ropp_Ropp_IZR z2); symmetry ; apply plus_IZR.
+  intros z1 z2; unfold Rminus,CRminus; unfold Z.sub.
+  rewrite <- (Ropp_Ropp_IZR z2); symmetry; apply plus_IZR.
 Qed.
 
 (**********)
@@ -1566,7 +2050,7 @@ Proof.
    subst n. rewrite <- INR_IZR_INZ. apply (lt_INR 0).
    apply Nat2Z.inj_lt. apply H. }
   intros. apply (Rplus_lt_reg_r (-(IZR n))).
-  pose proof minus_IZR. unfold CReal_minus in H0.
+  pose proof minus_IZR. unfold Rminus,CRminus 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.
@@ -1575,10 +2059,9 @@ Qed.
 (**********)
 Lemma not_0_IZR : forall n:Z, n <> 0%Z -> IZR n # 0.
 Proof.
-  intros. destruct (Z.lt_trichotomy n 0).
-  left. apply (IZR_lt n 0). exact H0.
-  destruct H0. contradiction.
-  right. apply (IZR_lt 0 n). exact H0.
+  intros. destruct n. exfalso. apply H. reflexivity.
+  right. apply (IZR_lt 0). reflexivity.
+  left. apply (IZR_lt _ 0). reflexivity.
 Qed.
 
 (*********)
@@ -1594,7 +2077,7 @@ Qed.
 Lemma le_IZR : forall n m:Z, IZR n <= IZR m -> (n <= m)%Z.
 Proof.
   intros. apply (Rplus_le_compat_r (-(IZR n))) in H.
-  pose proof minus_IZR. unfold CReal_minus in H0.
+  pose proof minus_IZR. unfold Rminus,CRminus in H0.
   repeat rewrite <- H0 in H. unfold Zminus in H.
   rewrite Z.add_opp_diag_r in H.
   apply (Z.add_le_mono_l _ _ (-n)). ring_simplify.
@@ -1610,22 +2093,27 @@ Qed.
 (**********)
 Lemma IZR_ge : forall n m:Z, (n >= m)%Z -> IZR n >= IZR m.
 Proof.
-  intros m n H; apply Rnot_lt_ge; red; intro.
-  generalize (lt_IZR m n H0); intro; omega.
+  intros m n H; apply Rnot_lt_ge. intro abs.
+  apply lt_IZR in abs. omega.
 Qed.
 
 Lemma IZR_le : forall n m:Z, (n <= m)%Z -> IZR n <= IZR m.
 Proof.
-  intros m n H; apply Rnot_gt_le; red; intro.
-  unfold CRealGt in H0; generalize (lt_IZR n m H0); intro; omega.
+  intros m n H; apply Rnot_lt_ge. intro abs.
+  apply lt_IZR in abs. omega.
 Qed.
 
 Lemma IZR_neq : forall z1 z2:Z, z1 <> z2 -> IZR z1 # IZR z2.
 Proof.
-  intros. destruct (Z.lt_trichotomy z1 z2).
-  left. apply IZR_lt. exact H0.
-  destruct H0. contradiction.
-  right. apply IZR_lt. exact H0.
+  intros. destruct (not_0_IZR (z1-z2)).
+  intro abs. apply H. rewrite <- (Z.add_cancel_r _ _ (-z2)).
+  ring_simplify. exact abs.
+  left. apply IZR_lt. apply (lt_IZR _ 0) in c.
+  rewrite (Z.add_lt_mono_r _ _ (-z2)).
+  ring_simplify. exact c.
+  right. apply IZR_lt. apply (lt_IZR 0) in c.
+  rewrite (Z.add_lt_mono_l _ _ (-z2)).
+  ring_simplify. rewrite Z.add_comm. exact c.
 Qed.
 
 Hint Extern 0 (IZR _ <= IZR _) => apply IZR_le, Zle_bool_imp_le, eq_refl : creal.
@@ -1649,7 +2137,7 @@ Proof.
   intros r z x [H1 H2] [H3 H4].
   cut ((z - x)%Z = 0%Z); auto with zarith.
   apply one_IZR_lt1.
-  rewrite <- Z_R_minus; split.
+  split; rewrite <- Z_R_minus.
   setoid_replace (-(1)) with (r - (r + 1)).
   unfold CReal_minus; apply Rplus_lt_le_compat; auto with creal.
   ring.
@@ -1672,18 +2160,13 @@ Lemma tech_single_z_r_R1 :
   forall r (n:Z),
     r < IZR n ->
     IZR n <= r + 1 ->
-    (exists s : Z, s <> n /\ r < IZR s /\ IZR s <= r + 1) -> False.
+    { s : Z & prod (s <> n) (r < IZR s <= r + 1) } -> False.
 Proof.
   intros r z H1 H2 [s [H3 [H4 H5]]].
   apply H3; apply single_z_r_R1 with r; trivial.
 Qed.
 
 
-
-(*********************************************************)
-(** ** Computable Reals                                  *)
-(*********************************************************)
-
 Lemma Rmult_le_compat_l_half : forall r r1 r2,
     0 < r -> r1 <= r2 -> r * r1 <= r * r2.
 Proof.
@@ -1691,6 +2174,72 @@ Proof.
   contradiction. apply H.
 Qed.
 
+Lemma INR_gen_phiZ : forall (n : nat),
+    gen_phiZ 0 1 Rplus Rmult Ropp (Z.of_nat n) == INR n.
+Proof.
+  induction n.
+  - apply Req_refl.
+  - replace (Z.of_nat (S n)) with (1 + Z.of_nat n)%Z.
+    rewrite (gen_phiZ_add Req_rel (CRisRingExt CR) RisRing).
+    rewrite IHn. clear IHn. simpl. rewrite (Rplus_comm 1).
+    destruct n. rewrite Rplus_0_l. reflexivity. reflexivity.
+    replace (S n) with (1 + n)%nat. 2: reflexivity.
+    rewrite (Nat2Z.inj_add 1 n). reflexivity.
+Qed.
+
+Definition Rup_nat (x : R)
+  : { n : nat & x < INR n }.
+Proof.
+  intros. destruct (CRarchimedean CR x) as [p maj].
+  destruct p.
+  - exists O. apply maj.
+  - exists (Pos.to_nat p).
+    rewrite <- positive_nat_Z, (INR_gen_phiZ (Pos.to_nat p)) in maj. exact maj.
+  - exists O. apply (Rlt_trans _ _ _ maj). simpl.
+    rewrite <- Ropp_0. apply Ropp_gt_lt_contravar.
+    fold (gen_phiZ 0 1 Rplus Rmult Ropp (Z.pos p)).
+    replace (gen_phiPOS 1 (CRplus CR) (CRmult CR) p)
+      with (gen_phiZ 0 1 Rplus Rmult Ropp (Z.pos p)).
+    2: reflexivity.
+    rewrite <- positive_nat_Z, (INR_gen_phiZ (Pos.to_nat p)).
+    apply (lt_INR 0). apply Pos2Nat.is_pos.
+Qed.
+
+Fixpoint Rarchimedean_ind (x:R) (n : Z) (p:nat) { struct p }
+  : (x < IZR n < x + 2 + (INR p))
+    -> { n:Z & x < IZR n < x+2 }.
+Proof.
+  destruct p.
+  - exists n. destruct H. split. exact r. rewrite Rplus_0_r in r0; exact r0.
+  - intros. destruct (linear_order_T (x+1+INR p) (IZR n) (x+2+INR p)).
+    do 2 rewrite Rplus_assoc. apply Rplus_lt_compat_l, Rplus_lt_compat_r.
+    rewrite <- (Rplus_0_r 1). apply Rplus_lt_compat_l. apply Rlt_0_1.
+    + apply (Rarchimedean_ind x (n-1)%Z p). unfold Zminus.
+      split; rewrite plus_IZR, opp_IZR.
+      setoid_replace (IZR 1) with 1. 2: reflexivity.
+      apply (Rplus_lt_reg_l 1). ring_simplify.
+      apply (Rle_lt_trans _ (x + 1 + INR p)). 2: exact r.
+      rewrite Rplus_assoc. apply Rplus_le_compat_l.
+      rewrite <- (Rplus_0_r 1), Rplus_assoc. apply Rplus_le_compat_l.
+      rewrite Rplus_0_l. apply (le_INR 0), le_0_n.
+      setoid_replace (IZR 1) with 1. 2: reflexivity.
+      apply (Rplus_lt_reg_l 1). ring_simplify.
+      setoid_replace (x + 2 + INR p + 1) with (x + 2 + INR (S p)).
+      apply H. rewrite S_INR. ring.
+    + apply (Rarchimedean_ind x n p). split. apply H. exact r.
+Qed.
+
+Lemma Rarchimedean (x:R) : { n : Z & x < IZR n < x + 2 }.
+Proof.
+  destruct (Rup_nat x) as [n nmaj].
+  destruct (Rup_nat (INR n + - (x + 2))) as [p pmaj].
+  apply (Rplus_lt_compat_r (x+2)) in pmaj.
+  rewrite Rplus_assoc, Rplus_opp_l, Rplus_0_r in pmaj.
+  apply (Rarchimedean_ind x (Z.of_nat n) p).
+  split; rewrite <- INR_IZR_INZ. exact nmaj.
+  rewrite Rplus_comm in pmaj. exact pmaj.
+Qed.
+
 Lemma Rmult_le_0_compat : forall a b,
     0 <= a -> 0 <= b -> 0 <= a * b.
 Proof.
@@ -1698,51 +2247,42 @@ Proof.
   intros. intro abs.
   assert (0 < -(a*b)) as epsPos.
   { rewrite <- Ropp_0. apply Ropp_gt_lt_contravar. apply abs. }
-  pose proof (Rarchimedean (b * (/ (-(a*b))) (or_intror (Ropp_0_gt_lt_contravar _ abs))))
-    as [n [maj _]].
-  destruct n as [|n|n].
+  pose proof (Rup_nat (b * (/ (-(a*b))) (inr (Ropp_0_gt_lt_contravar _ abs))))
+    as [n maj].
+  destruct n as [|n].
   - simpl in maj. apply (Rmult_lt_compat_r (-(a*b))) in maj.
     rewrite Rmult_0_l in maj.
     rewrite Rmult_assoc in maj. rewrite Rinv_l in maj.
     rewrite Rmult_1_r in maj. contradiction.
     apply epsPos.
   - (* n > 0 *)
-    assert (0 < IZR (Z.pos n)) as nPos.
-    apply (IZR_lt 0). reflexivity.
-    assert (b * (/ (IZR (Z.pos n))) (or_intror nPos) < -(a*b)).
-    { apply (Rmult_lt_reg_r (IZR (Z.pos n))). apply nPos.
+    assert (0 < INR (S n)) as nPos.
+    { apply (lt_INR 0). apply le_n_S, le_0_n. }
+    assert (b * (/ (INR (S n))) (inr nPos) < -(a*b)).
+    { apply (Rmult_lt_reg_r (INR (S n))). apply nPos.
       rewrite Rmult_assoc. rewrite Rinv_l.
       rewrite Rmult_1_r. apply (Rmult_lt_compat_r (-(a*b))) in maj.
       rewrite Rmult_assoc in maj. rewrite Rinv_l in maj.
       rewrite Rmult_1_r in maj. rewrite Rmult_comm.
       apply maj. exact epsPos. }
-    pose proof (Rmult_le_compat_l_half (a + (/ (IZR (Z.pos n))) (or_intror nPos))
+    pose proof (Rmult_le_compat_l_half (a + (/ (INR (S n))) (inr nPos))
                                        0 b).
-    assert (a + (/ (IZR (Z.pos n))) (or_intror nPos) > 0 + 0).
+    assert (a + (/ (INR (S n))) (inr nPos) > 0 + 0).
     apply Rplus_le_lt_compat. apply H. apply Rinv_0_lt_compat.
     rewrite Rplus_0_l in H3. specialize (H2 H3 H0).
     clear H3. rewrite Rmult_0_r in H2.
     apply H2. clear H2. rewrite Rmult_plus_distr_r.
     apply (Rplus_lt_compat_l (a*b)) in H1.
     rewrite Rplus_opp_r in H1.
-    rewrite (Rmult_comm ((/ (IZR (Z.pos n))) (or_intror nPos))).
+    rewrite (Rmult_comm ((/ (INR (S n))) (inr nPos))).
     apply H1.
-  - (* n < 0 *)
-    assert (b * (/ (- (a * b))) (or_intror (Ropp_0_gt_lt_contravar _ abs)) < 0).
-    apply (CRealLt_trans _ (IZR (Z.neg n)) _ maj).
-    apply Ropp_lt_cancel. rewrite Ropp_0.
-    rewrite <- opp_IZR. apply (IZR_lt 0). reflexivity.
-    apply (Rmult_lt_compat_r (-(a*b))) in H1.
-    rewrite Rmult_0_l in H1. rewrite Rmult_assoc in H1.
-    rewrite Rinv_l in H1. rewrite Rmult_1_r in H1. contradiction.
-    apply epsPos.
 Qed.
 
 Lemma Rmult_le_compat_l : forall r r1 r2,
     0 <= r -> r1 <= r2 -> r * r1 <= r * r2.
 Proof.
   intros. apply Rminus_ge. apply Rge_minus in H0.
-  unfold CReal_minus. rewrite Ropp_mult_distr_r.
+  unfold Rminus,CRminus. rewrite Ropp_mult_distr_r.
   rewrite <- Rmult_plus_distr_l.
   apply Rmult_le_0_compat; assumption.
 Qed.
@@ -1762,8 +2302,8 @@ Lemma Rmult_le_0_lt_compat :
     0 <= r1 -> 0 <= r3 -> r1 < r2 -> r3 < r4 -> r1 * r3 < r2 * r4.
 Proof.
   intros. apply (Rle_lt_trans _ (r2 * r3)).
-  apply Rmult_le_compat_r. apply H0. apply CRealLt_asym.
-  apply H1. apply Rmult_lt_compat_l. exact (Rle_lt_trans 0 r1 r2 H H1).
+  apply Rmult_le_compat_r. apply H0. intro abs. apply (Rlt_asym r1 r2 H1).
+  apply abs. apply Rmult_lt_compat_l. exact (Rle_lt_trans 0 r1 r2 H H1).
   exact H2.
 Qed.
 
@@ -1816,36 +2356,34 @@ Lemma Rmult_ge_compat :
     r2 >= 0 -> r4 >= 0 -> r1 >= r2 -> r3 >= r4 -> r1 * r3 >= r2 * r4.
 Proof. auto with creal rorders. Qed.
 
-Lemma IPR_double : forall p:positive, IPR (2*p) == 2 * IPR p.
-Proof.
-  intro p. destruct p.
-  - reflexivity.
-  - reflexivity.
-  - rewrite Rmult_1_r. reflexivity.
-Qed.
-
 Lemma mult_IPR_IZR : forall (n:positive) (m:Z), IZR (Z.pos n * m) == IPR n * IZR m.
 Proof.
   intros. rewrite mult_IZR. apply Rmult_eq_compat_r. reflexivity.
 Qed.
 
+Definition IQR (q:Q) : R :=
+  match q with
+  | Qmake a b => IZR a * (/ (IPR b)) (inr (IPR_pos b))
+  end.
+Arguments IQR q%Q : simpl never.
+
 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))).
+  setoid_replace ((/ IPR (Qden * Qden0)) (inr (IPR_pos (Qden * Qden0))))
+    with ((/ IPR Qden) (inr (IPR_pos Qden))
+          * (/ IPR Qden0) (inr (IPR_pos Qden0))).
   rewrite Rmult_plus_distr_r.
   repeat rewrite Rmult_assoc. rewrite <- (Rmult_assoc (IZR (Z.pos Qden))).
   rewrite Rinv_r. rewrite Rmult_1_l.
-  rewrite (Rmult_comm ((/IPR Qden) (or_intror (IPR_pos Qden)))).
+  rewrite (Rmult_comm ((/IPR Qden) (inr (IPR_pos Qden)))).
   rewrite <- (Rmult_assoc (IZR (Z.pos Qden0))).
   rewrite Rinv_r. rewrite Rmult_1_l. reflexivity. unfold IZR.
   right. apply IPR_pos.
   right. apply IPR_pos.
   rewrite <- (Rinv_mult_distr
-                _ _ _ _ (or_intror (Rmult_lt_0_compat _ _ (IPR_pos _) (IPR_pos _)))).
+                _ _ _ _ (inr (Rmult_lt_0_compat _ _ (IPR_pos _) (IPR_pos _)))).
   apply Rinv_eq_compat. apply mult_IPR.
 Qed.
 
@@ -1898,7 +2436,7 @@ Proof.
   apply Rmult_le_compat_l.
   apply (IZR_le 0 a). unfold Qle in H; simpl in H.
   rewrite Z.mul_1_r in H. apply H.
-  apply CRealLt_asym. apply Rinv_0_lt_compat.
+  unfold Rle. apply Rlt_asym. apply Rinv_0_lt_compat.
 Qed.
 
 Lemma IQR_le : forall n m:Q, Qle n m -> IQR n <= IQR m.
@@ -1910,7 +2448,7 @@ Proof.
 Qed.
 
 Add Parametric Morphism : IQR
-    with signature Qeq ==> CRealEq
+    with signature Qeq ==> Req
       as IQR_morph.
 Proof.
   intros. destruct x,y; unfold IQR; simpl.
@@ -1928,115 +2466,108 @@ Proof.
   right. apply IPR_pos.
 Qed.
 
-Definition Rup_nat (x : CReal)
-  : { n : nat | x < INR n }.
+Instance IQR_morph_T
+  : CMorphisms.Proper
+      (CMorphisms.respectful Qeq Req) IQR.
 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.
+  intros x y H. destruct x,y; unfold IQR.
+  unfold Qeq in H; simpl in H.
+  apply (Rmult_eq_reg_r (IZR (Z.pos Qden))).
+  2: right; apply IPR_pos.
+  rewrite Rmult_assoc, Rinv_l, Rmult_1_r.
+  rewrite (Rmult_comm (IZR Qnum0)).
+  apply (Rmult_eq_reg_l (IZR (Z.pos Qden0))).
+  2: right; apply IPR_pos.
+  rewrite <- Rmult_assoc, <- Rmult_assoc, Rinv_r.
+  rewrite Rmult_1_l.
+  repeat rewrite <- mult_IZR.
+  rewrite <- H. rewrite Zmult_comm. reflexivity.
+  right; apply IPR_pos.
 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 }
+Fixpoint Rfloor_pos (a : R) (n : nat) { struct n }
   : 0 < a
     -> a < INR n
-    -> { p : nat | INR p < a < INR p + 2 }.
+    -> { 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.
+  - exfalso. apply (Rlt_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 H. rewrite Rplus_0_l. apply (Rlt_trans a (1+0)).
+      rewrite Rplus_comm, Rplus_0_l. 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.
+      * rewrite <- Rplus_0_l, S_INR, Rplus_comm. apply Rplus_lt_compat_l.
         apply Rlt_0_1.
-      * exists p. split. exact c.
+      * exists p. split. exact r.
         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. }
+      * apply (Rfloor_pos a n H). rewrite des. apply r.
+Qed.
+
+Definition Rfloor (a : R)
+  : { p : Z & IZR p < a < IZR p + 2 }.
+Proof.
   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.
+  - destruct (Rup_nat a). destruct (Rfloor_pos a x r r0).
+    exists (Z.of_nat x0). split; rewrite <- INR_IZR_INZ; apply p.
+  - apply (Rplus_lt_compat_l (-a)) in r.
+    rewrite Rplus_comm, Rplus_opp_r, Rplus_comm in r.
+    destruct (Rup_nat (1-a)).
+    destruct (Rfloor_pos (1-a) x r r0).
+    exists (-(Z.of_nat x0 + 1))%Z. split; rewrite opp_IZR, plus_IZR.
     + rewrite <- (Ropp_involutive a). apply Ropp_gt_lt_contravar.
-      destruct a0 as [_ a0]. apply (Rplus_lt_reg_r 1).
+      destruct p 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.
+    + destruct p as [a0 _]. apply (Rplus_lt_compat_l a) in a0.
+      unfold Rminus in a0.
+      rewrite <- (Rplus_comm (1+-a)), Rplus_assoc, Rplus_opp_l, Rplus_0_r 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 }.
+   a and a+1/n). This is how real numbers compute,
+   and they are measured by exact rational numbers. *)
+Definition RQ_dense (a b : R)
+  : a < b -> { q : Q & a < IQR q < b }.
 Proof.
-  intros H H0.
+  intros 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].
+  pose proof (Rup_nat ((/(b-a)) (inr epsPos)))
+    as [n maj].
+  destruct n as [|k].
   - 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.
+    apply (Rlt_asym 0 1). apply Rlt_0_1. apply maj.
+    right. apply epsPos.
   - (* 0 < n *)
+    pose (Pos.of_nat (S k)) as 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 (Rlt_trans a (b - IQR (1 # n))).
       apply (Rplus_lt_reg_r (IQR (1#n))).
-      unfold CReal_minus. rewrite Rplus_assoc. rewrite Rplus_opp_l.
+      unfold Rminus,CRminus. 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_assoc, Rplus_opp_l, 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.
+      rewrite Rmult_1_l. apply (Rmult_lt_reg_l (IPR n)).
+      apply IPR_pos. rewrite Rinv_r.
+      apply (Rmult_lt_compat_l (b-a)) in maj.
+      rewrite Rinv_r, Rmult_comm in maj.
+      rewrite <- INR_IPR. unfold n. rewrite Nat2Pos.id.
+      apply maj. discriminate. right. exact epsPos. exact epsPos.
       right. apply IPR_pos.
       apply (Rplus_lt_reg_r (IQR (1 # n))).
-      unfold CReal_minus. rewrite Rplus_assoc. rewrite Rplus_opp_l.
+      unfold Rminus,CRminus. rewrite Rplus_assoc, Rplus_opp_l.
       rewrite Rplus_0_r. rewrite <- plus_IQR.
       destruct maj2 as [_ maj2].
       setoid_replace ((p # 2 * n) + (1 # n))%Q
@@ -2046,47 +2577,95 @@ Proof.
       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.
+      apply Qinv_plus_distr.
     + 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.
+      apply (IZR_lt 0). apply Pos2Z.is_pos. rewrite Rmult_assoc, Rinv_l.
+      rewrite Rmult_1_r, Rmult_comm. apply maj2.
+Qed.
+
+Definition RQ_limit : forall (x : R) (n:nat),
+    { q:Q & x < IQR q < x + IQR (1 # Pos.of_nat n) }.
+Proof.
+  intros x n. apply (RQ_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.
+  reflexivity.
 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.
+(* Rlt is decided by the LPO in Type,
+   which is a non-constructive oracle. *)
+Lemma Rlt_lpo_dec : forall x y : R,
+    (forall (P : nat -> Prop), (forall n, {P n} + {~P n})
+                    -> {n | ~P n} + {forall n, P n})
+    -> (x < y) + (y <= x).
+Proof.
+  intros x y lpo.
+  pose (fun n => let (l,_) := RQ_limit x n in l) as xn.
+  pose (fun n => let (l,_) := RQ_limit y n in l) as yn.
+  destruct (lpo (fun n:nat => Qle (yn n - xn n) (1 # Pos.of_nat n))).
+  - intro n. destruct (Qlt_le_dec (1 # Pos.of_nat n) (yn n - xn n)).
+    right. apply Qlt_not_le. exact q. left. exact q.
+  - left. destruct s as [n nmaj]. unfold xn,yn in nmaj.
+    destruct (RQ_limit x n), (RQ_limit y n); unfold proj1_sig in nmaj.
+    apply Qnot_le_lt in nmaj.
+    apply (Rlt_le_trans x (IQR x0)). apply p.
+    apply (Rle_trans _ (IQR (x1 - (1# Pos.of_nat n)))).
+    apply IQR_le. apply (Qplus_le_l _ _ ((1#Pos.of_nat n) - x0)).
+    ring_simplify. ring_simplify in nmaj. rewrite Qplus_comm.
+    apply Qlt_le_weak. exact nmaj.
+    unfold Qminus. rewrite plus_IQR,opp_IQR.
+    apply (Rplus_le_reg_r (IQR (1#Pos.of_nat n))).
+    ring_simplify. unfold Rle. apply Rlt_asym. rewrite Rplus_comm. apply p0.
+  - right. intro abs.
+    pose ((y - x) * IQR (1#2)) as eps.
+    assert (0 < eps) as epsPos.
+    { apply Rmult_lt_0_compat. apply Rgt_minus. exact abs.
+      apply IQR_pos. reflexivity. }
+    destruct (Rup_nat ((/eps) (inr epsPos))) as [n nmaj].
+    specialize (q (S n)). unfold xn, yn in q.
+    destruct (RQ_limit x (S n)) as [a amaj], (RQ_limit y (S n)) as [b bmaj];
+      unfold proj1_sig in q.
+    assert (IQR (1 # Pos.of_nat (S n)) < eps).
+    { unfold IQR. rewrite Rmult_1_l.
+      apply (Rmult_lt_reg_l (IPR (Pos.of_nat (S n)))). apply IPR_pos.
+      rewrite Rinv_r, <- INR_IPR, Nat2Pos.id. 2: discriminate.
+      apply (Rlt_trans _ _ (INR (S n))) in nmaj.
+      apply (Rmult_lt_compat_l eps) in nmaj.
+      rewrite Rinv_r, Rmult_comm in nmaj. exact nmaj.
+      right. exact epsPos. exact epsPos. apply lt_INR. apply le_n_S, le_refl.
+      right. apply IPR_pos. }
+    unfold eps in H. apply (Rlt_asym y (IQR b)).
+    + apply bmaj.
+    + apply (Rlt_le_trans _ (IQR a + (y - x) * IQR (1 # 2))).
+      apply IQR_le in q.
+      apply (Rle_lt_trans _ _ _ q) in H.
+      apply (Rplus_lt_reg_l (-IQR a)).
+      rewrite <- Rplus_assoc, Rplus_opp_l, Rplus_0_l, Rplus_comm,
+      <- opp_IQR, <- plus_IQR. exact H.
+      apply (Rplus_lt_compat_l x) in H.
+      destruct amaj. apply (Rlt_trans _ _ _ r0) in H.
+      apply (Rplus_lt_compat_r ((y - x) * IQR (1 # 2))) in H.
+      unfold Rle. apply Rlt_asym.
+      setoid_replace (x + (y - x) * IQR (1 # 2) + (y - x) * IQR (1 # 2)) with y in H.
+      exact H.
+      rewrite Rplus_assoc, <- Rmult_plus_distr_r.
+      setoid_replace (y - x + (y - x)) with ((y-x)*2).
+      unfold IQR. rewrite Rmult_1_l, Rmult_assoc, Rinv_r. ring.
+      right. apply (IZR_lt 0). reflexivity.
+      unfold IZR, IPR, IPR_2. ring.
+Qed.
+
+Lemma Rlt_lpo_floor : forall x : R,
+    (forall (P : nat -> Prop), (forall n, {P n} + {~P n})
+                    -> {n | ~P n} + {forall n, P n})
+    -> { p : Z & IZR p <= x < IZR p + 1 }.
+Proof.
+  intros x lpo. destruct (Rfloor x) as [n [H H0]].
+  destruct (Rlt_lpo_dec x (IZR n + 1) lpo).
+  - exists n. split. unfold Rle. apply Rlt_asym. exact H. exact r.
+  - exists (n+1)%Z. split. rewrite plus_IZR. exact r.
+    rewrite plus_IZR, Rplus_assoc. exact H0.
 Qed.
 
 
@@ -2099,7 +2678,7 @@ Qed.
 
 Lemma Rinv_le_contravar :
   forall x y (xpos : 0 < x) (ynz : y # 0),
-    x <= y -> (/ y) ynz <= (/ x) (or_intror xpos).
+    x <= y -> (/ y) ynz <= (/ x) (inr xpos).
 Proof.
   intros. intro abs. apply (Rmult_lt_compat_l x) in abs.
   2: apply xpos. rewrite Rinv_r in abs.
@@ -2111,7 +2690,7 @@ Proof.
 Qed.
 
 Lemma Rle_Rinv : forall x y (xpos : 0 < x) (ypos : 0 < y),
-    x <= y -> (/ y) (or_intror ypos) <= (/ x) (or_intror xpos).
+    x <= y -> (/ y) (inr ypos) <= (/ x) (inr xpos).
 Proof.
   intros.
   apply Rinv_le_contravar with (1 := H).
@@ -2130,12 +2709,12 @@ Qed.
 
 Lemma Rlt_0_2 : 0 < 2.
 Proof.
-  apply (CRealLt_trans 0 (0+1)). rewrite Rplus_0_l. exact Rlt_0_1.
+  apply (Rlt_trans 0 (0+1)). rewrite Rplus_0_l. exact Rlt_0_1.
   apply Rplus_lt_le_compat. exact Rlt_0_1. apply Rle_refl.
 Qed.
 
-Lemma double_var : forall r1, r1 == r1 * (/ 2) (or_intror Rlt_0_2)
-                                    + r1 * (/ 2) (or_intror Rlt_0_2).
+Lemma double_var : forall r1, r1 == r1 * (/ 2) (inr Rlt_0_2)
+                                    + r1 * (/ 2) (inr Rlt_0_2).
 Proof.
   intro; rewrite <- double; rewrite <- Rmult_assoc;
     symmetry ; apply Rinv_r_simpl_m.
@@ -2143,7 +2722,7 @@ Qed.
 
 (* IZR : Z -> R is a ring morphism *)
 Lemma R_rm : ring_morph
-  0 1 CReal_plus CReal_mult CReal_minus CReal_opp CRealEq
+  0 1 Rplus Rmult Rminus Ropp Req
   0%Z 1%Z Zplus Zmult Zminus Z.opp Zeq_bool IZR.
 Proof.
 constructor ; try easy.
@@ -2174,7 +2753,7 @@ Lemma Rmult_ge_0_gt_0_lt_compat :
     r3 >= 0 -> r2 > 0 -> r1 < r2 -> r3 < r4 -> r1 * r3 < r2 * r4.
 Proof.
   intros. apply (Rle_lt_trans _ (r2 * r3)).
-  apply Rmult_le_compat_r. apply H. apply CRealLt_asym. apply H1.
+  apply Rmult_le_compat_r. apply H. unfold Rle. apply Rlt_asym. apply H1.
   apply Rmult_lt_compat_l. apply H0. apply H2.
 Qed.
 
@@ -2182,11 +2761,11 @@ Lemma le_epsilon :
   forall r1 r2, (forall eps, 0 < eps -> r1 <= r2 + eps) -> r1 <= r2.
 Proof.
   intros x y H. intro abs.
-  assert (0 < (x - y) * (/ 2) (or_intror Rlt_0_2)).
+  assert (0 < (x - y) * (/ 2) (inr Rlt_0_2)).
   { apply (Rplus_lt_compat_r (-y)) in abs. rewrite Rplus_opp_r in abs.
     apply Rmult_lt_0_compat. exact abs.
     apply Rinv_0_lt_compat. }
-  specialize (H ((x - y) * (/ 2) (or_intror Rlt_0_2)) H0).
+  specialize (H ((x - y) * (/ 2) (inr Rlt_0_2)) H0).
   apply (Rmult_le_compat_l 2) in H.
   rewrite Rmult_plus_distr_l in H.
   apply (Rplus_le_compat_l (-x)) in H.
@@ -2194,12 +2773,12 @@ Proof.
   (Rmult_plus_distr_r 1 1), (Rmult_plus_distr_r 1 1)
     in H.
   ring_simplify in H; contradiction.
-  right. apply Rlt_0_2. apply CRealLt_asym. apply Rlt_0_2.
+  right. apply Rlt_0_2. unfold Rle. apply Rlt_asym. apply Rlt_0_2.
 Qed.
 
 (**********)
 Lemma Rdiv_lt_0_compat : forall a b (bpos : 0 < b),
-    0 < a -> 0 < a * (/b) (or_intror bpos).
+    0 < a -> 0 < a * (/b) (inr bpos).
 Proof.
 intros; apply Rmult_lt_0_compat;[|apply Rinv_0_lt_compat]; assumption.
 Qed.
@@ -2213,7 +2792,9 @@ Qed.
 Lemma Rdiv_minus_distr : forall a b c (cnz : c # 0),
     (a - b)* (/c) cnz == a* (/c) cnz - b* (/c) cnz.
 Proof.
-  intros; unfold CReal_minus; rewrite Rmult_plus_distr_r; ring.
+  intros; unfold Rminus,CRminus; rewrite Rmult_plus_distr_r.
+  apply Rplus_morph. reflexivity.
+  rewrite Ropp_mult_distr_l. reflexivity.
 Qed.
 
 
@@ -2222,14 +2803,14 @@ Qed.
 (*********************************************************)
 
 Record nonnegreal : Type := mknonnegreal
-  {nonneg :> CReal; cond_nonneg : 0 <= nonneg}.
+  {nonneg :> R; cond_nonneg : 0 <= nonneg}.
 
-Record posreal : Type := mkposreal {pos :> CReal; cond_pos : 0 < pos}.
+Record posreal : Type := mkposreal {pos :> R; cond_pos : 0 < pos}.
 
 Record nonposreal : Type := mknonposreal
-  {nonpos :> CReal; cond_nonpos : nonpos <= 0}.
+  {nonpos :> R; cond_nonpos : nonpos <= 0}.
 
-Record negreal : Type := mknegreal {neg :> CReal; cond_neg : neg < 0}.
+Record negreal : Type := mknegreal {neg :> R; cond_neg : neg < 0}.
 
 Record nonzeroreal : Type := mknonzeroreal
-  {nonzero :> CReal; cond_nonzero : nonzero <> 0}.
+  {nonzero :> R; cond_nonzero : nonzero <> 0}.
diff --git a/theories/Reals/ConstructiveRcomplete.v b/theories/Reals/ConstructiveRcomplete.v
index 9fb98a528b..ce45bcd567 100644
--- a/theories/Reals/ConstructiveRcomplete.v
+++ b/theories/Reals/ConstructiveRcomplete.v
@@ -12,16 +12,16 @@
 Require Import QArith_base.
 Require Import Qabs.
 Require Import ConstructiveCauchyReals.
-Require Import ConstructiveRIneq.
+Require Import Logic.ConstructiveEpsilon.
 
-Local Open Scope R_scope_constr.
+Local Open Scope CReal_scope.
 
-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))))
-    -> (CRealLt (CReal_opp x) y /\ CRealLt y x).
+Lemma CReal_absSmall : forall (x y : CReal) (n : positive),
+    (Qlt (2 # 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.
+  intros x y n maj. split.
   - exists n. destruct x as [xn caux], y as [yn cauy]; simpl.
     simpl in maj. unfold Qminus. rewrite Qopp_involutive.
     rewrite Qplus_comm.
@@ -35,120 +35,191 @@ Proof.
     apply maj. apply Qplus_le_r. apply Qopp_le_compat. apply Qle_Qabs.
 Qed.
 
+Definition absSmall (a b : CReal) : Set
+  := -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. split.
+  rewrite <- seq. apply H0. apply H.
+  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). split; rewrite <- INR_IZR_INZ; apply p.
+  - 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. split; rewrite opp_IZR, plus_IZR.
+    + rewrite <- (CReal_opp_involutive a). apply CReal_opp_gt_lt_contravar.
+      destruct p as [_ a0]. apply (CReal_plus_lt_reg_r 1).
+      rewrite CReal_plus_comm, CReal_plus_assoc. rewrite <- INR_IZR_INZ. apply a0.
+    + destruct p as [a0 _]. apply (CReal_plus_lt_compat_l a) in a0.
+      unfold CReal_minus in a0.
+      rewrite <- (CReal_plus_comm (1+-a)), CReal_plus_assoc, CReal_plus_opp_l, CReal_plus_0_r 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.
+Definition Rup_nat (x : CReal)
+  : { n : nat & x < INR n }.
 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. 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.
 
-(** 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.
+(* 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.
-  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 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 (Rup_nat ((/(b-a)) (inr epsPos)))
+    as [n maj].
+  destruct n as [|k].
+  - 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 *)
+    pose (Pos.of_nat (S k)) as 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 (IPR n)).
+      apply IPR_pos. rewrite CReal_inv_r.
+      apply (CReal_mult_lt_compat_l (b-a)) in maj.
+      rewrite CReal_inv_r, CReal_mult_comm in maj.
+      rewrite <- INR_IPR. unfold n. rewrite Nat2Pos.id.
+      apply maj. discriminate. 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.
 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 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 (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 RQ_limit : forall (x : CReal) (n:nat),
-    { q:Q | x < IQR q < x + IQR (1 # Pos.of_nat n) }.
+    { 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.
 
@@ -160,7 +231,7 @@ Definition Un_cauchy_Q (xn : nat -> Q) : Set
 
 Lemma Rdiag_cauchy_sequence : forall (xn : nat -> CReal),
     Un_cauchy_mod xn
-    -> Un_cauchy_Q (fun n => proj1_sig (RQ_limit (xn n) n)).
+    -> Un_cauchy_Q (fun n => let (l,_) := RQ_limit (xn n) n in l).
 Proof.
   intros xn H p. specialize (H (2 * p)%positive) as [k cv].
   exists (max k (2 * Pos.to_nat p)). intros.
@@ -171,60 +242,71 @@ 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 opp_IQR. exact c.
       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.
-      destruct (RQ_limit (xn p0) p0); simpl. apply a.
+    + rewrite plus_IQR. apply CReal_plus_le_lt_compat.
+      apply CRealLt_asym.
+      destruct (RQ_limit (xn p0) p0); simpl. apply p1.
       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 p1. 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))).
         2: apply H0. replace (p~0)%positive with (2*p)%positive.
         2: reflexivity. rewrite Pos2Nat.inj_mul.
         apply Nat.le_max_r. }
-      rewrite Nat2Pos.id. apply H3. intro abs. subst q.
-      inversion H3. pose proof (Pos2Nat.is_pos (p~0)).
-      rewrite H5 in H4. inversion H4.
+      rewrite Nat2Pos.id. apply H1. intro abs. subst q.
+      inversion H1. pose proof (Pos2Nat.is_pos (p~0)).
+      rewrite H3 in H2. inversion H2.
   - 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 p1. 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))).
         2: apply H. replace (p~0)%positive with (2*p)%positive.
         2: reflexivity. rewrite Pos2Nat.inj_mul.
         apply Nat.le_max_r. }
-      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.
-      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.
+      rewrite Nat2Pos.id. apply H1. intro abs. subst p0.
+      inversion H1. pose proof (Pos2Nat.is_pos (p~0)).
+      rewrite H3 in H2. inversion H2.
+      rewrite opp_IQR. apply CReal_opp_gt_lt_contravar.
+      destruct (RQ_limit (xn q) q); simpl. apply p1.
+    + 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.
+      exact c0. rewrite Qplus_comm.
       setoid_replace (1#p)%Q with (2 # 2*p)%Q. rewrite Qinv_minus_distr.
       reflexivity. reflexivity.
 Qed.
 
+Lemma doubleLtCovariant : forall a b c d e f : CReal,
+    a == b -> c == d -> e == f
+    -> (a < c < e)
+    -> (b < d < f).
+Proof.
+  split. rewrite <- H. rewrite <- H0. apply H2.
+  rewrite <- H0. rewrite <- H1. apply H2.
+Qed.
+
 (* An element of CReal is a Cauchy sequence of rational numbers,
    show that it converges to itself in CReal. *)
 Lemma CReal_cv_self : forall (qn : nat -> Q) (x : CReal) (cvmod : positive -> nat),
@@ -233,11 +315,12 @@ 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.
-  setoid_replace (IQR (qn p0)) with (inject_Q (qn p0)).
-  2: apply FinjectQ_CReal.
-  apply CReal_absSmall.
-  exists (Pos.max (4 * p)%positive (Pos.of_nat (cvmod (2 * p)%positive))).
+  intros p0 H0. unfold absSmall, CReal_minus.
+  apply (doubleLtCovariant (-inject_Q (1#p)) _ (inject_Q (qn p0) - x) _ (inject_Q (1#p))).
+  rewrite FinjectQ_CReal. reflexivity.
+  rewrite FinjectQ_CReal. reflexivity.
+  rewrite FinjectQ_CReal. reflexivity.
+  apply (CReal_absSmall _ _ (Pos.max (4 * p)%positive (Pos.of_nat (cvmod (2 * p)%positive)))).
   setoid_replace (proj1_sig (inject_Q (1 # p)) (Pos.to_nat (Pos.max (4 * p) (Pos.of_nat (cvmod (2 * p)%positive)))))
     with (1 # p)%Q.
   2: reflexivity.
@@ -246,12 +329,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 +353,8 @@ 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.
+  split; rewrite <- (H0 i); apply cv; apply H1.
 Qed.
 
 (* Q is dense in Archimedean fields, so all real numbers
@@ -284,8 +371,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))).
@@ -300,28 +387,29 @@ Lemma Rcauchy_complete : forall (xn : nat -> CReal),
     -> { l : CReal & Un_cv_mod xn l }.
 Proof.
   intros xn cau.
-  destruct (R_has_all_rational_limits (fun n => proj1_sig (RQ_limit (xn n) n))
+  destruct (R_has_all_rational_limits (fun n => let (l,_) := RQ_limit (xn n) n in l)
                                       (Rdiag_cauchy_sequence xn cau))
     as [l cv].
   exists l. intro p. specialize (cv (2*p)%positive) as [k cv].
   exists (max k (2 * Pos.to_nat p)). intros p0 H. specialize (cv p0).
-  destruct cv. apply (le_trans _ (max k (2 * Pos.to_nat p))).
+  destruct cv as [H0 H1]. apply (le_trans _ (max k (2 * Pos.to_nat p))).
   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 +420,13 @@ 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.
diff --git a/theories/Reals/ConstructiveReals.v b/theories/Reals/ConstructiveReals.v
new file mode 100644
index 0000000000..fc3d6afe15
--- /dev/null
+++ b/theories/Reals/ConstructiveReals.v
@@ -0,0 +1,149 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+(************************************************************************)
+
+(* An interface for constructive and computable real numbers.
+   All of its instances are isomorphic, for example it contains
+   the Cauchy reals implemented in file ConstructivecauchyReals
+   and the sumbool-based Dedekind reals defined by
+
+Structure R := {
+  (* The cuts are represented as propositional functions, rather than subsets,
+     as there are no subsets in type theory. *)
+  lower : Q -> Prop;
+  upper : Q -> Prop;
+  (* The cuts respect equality on Q. *)
+  lower_proper : Proper (Qeq ==> iff) lower;
+  upper_proper : Proper (Qeq ==> iff) upper;
+  (* The cuts are inhabited. *)
+  lower_bound : { q : Q | lower q };
+  upper_bound : { r : Q | upper r };
+  (* The lower cut is a lower set. *)
+  lower_lower : forall q r, q < r -> lower r -> lower q;
+  (* The lower cut is open. *)
+  lower_open : forall q, lower q -> exists r, q < r /\ lower r;
+  (* The upper cut is an upper set. *)
+  upper_upper : forall q r, q < r -> upper q -> upper r;
+  (* The upper cut is open. *)
+  upper_open : forall r, upper r -> exists q,  q < r /\ upper q;
+  (* The cuts are disjoint. *)
+  disjoint : forall q, ~ (lower q /\ upper q);
+  (* There is no gap between the cuts. *)
+  located : forall q r, q < r -> { lower q } + { upper r }
+}.
+
+  see github.com/andrejbauer/dedekind-reals for the Prop-based
+  version of those Dedekind reals (although Prop fails to make
+  them an instance of ConstructiveReals). *)
+
+Require Import QArith.
+
+Definition isLinearOrder (X : Set) (Xlt : X -> X -> Set) : Set
+  := (forall x y:X, Xlt x y -> Xlt y x -> False)
+     * (forall x y z : X, Xlt x y -> Xlt y z -> Xlt x z)
+     * (forall x y z : X, Xlt x z -> Xlt x y + Xlt y z).
+
+Definition orderEq (X : Set) (Xlt : X -> X -> Set) (x y : X) : Prop
+  := (Xlt x y -> False) /\ (Xlt y x -> False).
+
+Definition orderAppart (X : Set) (Xlt : X -> X -> Set) (x y : X) : Set
+  := Xlt x y  +  Xlt y x.
+
+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, { ~~P } + { ~P }.
+
+Record ConstructiveReals : Type :=
+  {
+    CRcarrier : Set;
+    CRlt : CRcarrier -> CRcarrier -> Set;
+    CRltLinear : isLinearOrder CRcarrier CRlt;
+
+    CRltProp : CRcarrier -> CRcarrier -> Prop;
+    (* This choice algorithm can be slow, keep it for the classical
+       quotient of the reals, where computations are blocked by
+       axioms like LPO. *)
+    CRltEpsilon : forall x y : CRcarrier, CRltProp x y -> CRlt x y;
+    CRltForget : forall x y : CRcarrier, CRlt x y -> CRltProp x y;
+    CRltDisjunctEpsilon : forall a b c d : CRcarrier,
+        (CRltProp a b \/ CRltProp c d) -> CRlt a b  +  CRlt c d;
+
+    (* Constants *)
+    CRzero : CRcarrier;
+    CRone : CRcarrier;
+
+    (* Addition and multiplication *)
+    CRplus : CRcarrier -> CRcarrier -> CRcarrier;
+    CRopp : CRcarrier -> CRcarrier; (* Computable opposite,
+                         stronger than Prop-existence of opposite *)
+    CRmult : CRcarrier -> CRcarrier -> CRcarrier;
+
+    CRisRing : ring_theory CRzero CRone CRplus CRmult
+                          (fun x y => CRplus x (CRopp y)) CRopp (orderEq CRcarrier CRlt);
+    CRisRingExt : ring_eq_ext CRplus CRmult CRopp (orderEq CRcarrier CRlt);
+
+    (* Compatibility with order *)
+    CRzero_lt_one : CRlt CRzero CRone; (* 0 # 1 would only allow 0 < 1 because
+                                    of Fmult_lt_0_compat so request 0 < 1 directly. *)
+    CRplus_lt_compat_l : forall r r1 r2 : CRcarrier,
+        CRlt r1 r2 -> CRlt (CRplus r r1) (CRplus r r2);
+    CRplus_lt_reg_l : forall r r1 r2 : CRcarrier,
+        CRlt (CRplus r r1) (CRplus r r2) -> CRlt r1 r2;
+    CRmult_lt_0_compat : forall x y : CRcarrier,
+        CRlt CRzero x -> CRlt CRzero y -> CRlt CRzero (CRmult x y);
+
+    (* A constructive total inverse function on F would need to be continuous,
+       which is impossible because we cannot connect plus and minus infinities.
+       Therefore it has to be a partial function, defined on non zero elements.
+       For this reason we cannot use Coq's field_theory and field tactic.
+
+       To implement Finv by Cauchy sequences we need orderAppart,
+       ~orderEq is not enough. *)
+    CRinv : forall x : CRcarrier, orderAppart _ CRlt x CRzero -> CRcarrier;
+    CRinv_l : forall (r:CRcarrier) (rnz : orderAppart _ CRlt r CRzero),
+        orderEq _ CRlt (CRmult (CRinv r rnz) r) CRone;
+    CRinv_0_lt_compat : forall (r : CRcarrier) (rnz : orderAppart _ CRlt r CRzero),
+        CRlt CRzero r -> CRlt CRzero (CRinv r rnz);
+
+    CRarchimedean : forall x : CRcarrier,
+        { k : Z & CRlt x (gen_phiZ CRzero CRone CRplus CRmult CRopp k) };
+
+    CRminus (x y : CRcarrier) : CRcarrier
+    := CRplus x (CRopp y);
+    CR_cv (un : nat -> CRcarrier) (l : CRcarrier) : Set
+    := forall eps:CRcarrier,
+        CRlt CRzero eps
+        -> { p : nat & forall i:nat, le p i -> CRlt (CRopp eps) (CRminus (un i) l)
+                                               * CRlt (CRminus (un i) l) eps };
+    CR_cauchy (un : nat -> CRcarrier) : Set
+    := forall eps:CRcarrier,
+        CRlt CRzero eps
+        -> { p : nat & forall i j:nat, le p i -> le p j ->
+                                       CRlt (CRopp eps) (CRminus (un i) (un j))
+                                       * CRlt (CRminus (un i) (un j)) eps };
+
+    CR_complete :
+      forall xn : nat -> CRcarrier, CR_cauchy xn -> { l : CRcarrier & CR_cv xn l };
+
+    (* Those are redundant, they could be proved from the previous hypotheses *)
+    CRis_upper_bound (E:CRcarrier -> Prop) (m:CRcarrier)
+    := forall x:CRcarrier, E x -> CRlt m x -> False;
+
+    CR_sig_lub :
+      forall (E:CRcarrier -> Prop),
+        sig_forall_dec_T
+        -> sig_not_dec_T
+        -> (exists x : CRcarrier, E x)
+        -> (exists x : CRcarrier, CRis_upper_bound E x)
+        -> { u : CRcarrier | CRis_upper_bound E u /\
+                             forall y:CRcarrier, CRis_upper_bound E y -> CRlt y u -> False };
+  }.
diff --git a/theories/Reals/ConstructiveRealsLUB.v b/theories/Reals/ConstructiveRealsLUB.v
new file mode 100644
index 0000000000..f5c447f7db
--- /dev/null
+++ b/theories/Reals/ConstructiveRealsLUB.v
@@ -0,0 +1,276 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+(************************************************************************)
+
+(* Proof that LPO and the excluded middle for negations imply
+   the existence of least upper bounds for all non-empty and bounded
+   subsets of the real numbers. *)
+
+Require Import QArith_base.
+Require Import Qabs.
+Require Import ConstructiveCauchyReals.
+Require Import ConstructiveRcomplete.
+Require Import Logic.ConstructiveEpsilon.
+
+Local Open Scope CReal_scope.
+
+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, { ~~P } + { ~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 E x lpo sig_not_dec.
+  destruct (sig_not_dec (~exists y:CReal, E y /\ CRealLtProp x y)).
+  - left. intros y H.
+    destruct (CRealLt_lpo_dec x y lpo). 2: exact f.
+    exfalso. apply n. intro abs. apply abs.
+    exists y. split. exact H. destruct c. exists x0. exact q.
+  - right. intro abs. apply n. intros [y [H H0]].
+    specialize (abs y H). apply CRealLtEpsilon in H0. contradiction.
+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 E lpo sig_not_dec Ebound.
+  apply constructive_indefinite_ground_description_nat.
+  - intro n. apply is_upper_bound_dec. exact lpo. exact sig_not_dec.
+  - destruct Ebound 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 E sig_not_dec lpo Einhab Ebound.
+  destruct (is_upper_bound_epsilon E lpo sig_not_dec Ebound) as [a luba].
+  destruct (is_upper_bound_not_epsilon E lpo sig_not_dec Einhab) 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 lpo. exact sig_not_dec. }
+  assert (forall q r : Q, (q <= r)%Q -> upcut q -> upcut r).
+  { intros. intros x Ex. specialize (H1 x Ex). intro abs.
+    apply H1. apply (CRealLe_Lt_trans _ (IQR r)). 2: exact abs.
+    apply IQR_le. exact H0. }
+  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 (H4 x Ex). rewrite <- H3. exact H4. }
+  destruct (glb_dec_Q (Build_DedekindDecCut
+                         upcut H3 (-Z.of_nat b # 1)%Q (Z.of_nat a # 1)
+                         H H0 H1 H2)).
+  simpl in a0. exists x. intro r. split.
+  - intros. apply a0. exact H4.
+  - 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.
+
+Lemma sig_lub :
+  forall (E:CReal -> Prop),
+    sig_forall_dec_T
+    -> sig_not_dec_T
+    -> (exists x : CReal, E x)
+    -> (exists x : CReal, is_upper_bound E x)
+    -> { u : CReal | is_lub E u }.
+Proof.
+  intros E sig_forall_dec sig_not_dec Einhab Ebound.
+  pose proof (is_upper_bound_closed E sig_forall_dec sig_not_dec Einhab Ebound).
+  destruct (is_upper_bound_glb
+              E sig_not_dec sig_forall_dec Einhab Ebound); simpl in H.
+  exists x. exact H.
+Qed.
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index 72475b79d7..75298855b2 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -543,7 +543,7 @@ Lemma Rmult_eq_reg_l : forall r r1 r2, r * r1 = r * r2 -> r <> 0 -> r1 = r2.
 Proof.
   intros. apply Rquot1. apply (Rmult_eq_reg_l (Rrepr r)).
   rewrite <- Rrepr_mult, <- Rrepr_mult, H. reflexivity.
-  rewrite Rrepr_appart, Rrepr_0 in H0. exact H0.
+  apply Rrepr_appart in H0. rewrite Rrepr_0 in H0. exact H0.
 Qed.
 
 Lemma Rmult_eq_reg_r : forall r r1 r2, r1 * r = r2 * r -> r <> 0 -> r1 = r2.
@@ -996,15 +996,16 @@ Qed.
 
 Lemma Rplus_lt_reg_l : forall r r1 r2, r + r1 < r + r2 -> r1 < r2.
 Proof.
-  intros. rewrite Rlt_def. apply (Rplus_lt_reg_l (Rrepr r)).
+  intros. rewrite Rlt_def. apply Rlt_forget. apply (Rplus_lt_reg_l (Rrepr r)).
   rewrite <- Rrepr_plus, <- Rrepr_plus.
-  rewrite Rlt_def in H. exact H.
+  rewrite Rlt_def in H. apply Rlt_epsilon. exact H.
 Qed.
 
 Lemma Rplus_lt_reg_r : forall r r1 r2, r1 + r < r2 + r -> r1 < r2.
 Proof.
-  intros. rewrite Rlt_def. apply (Rplus_lt_reg_r (Rrepr r)).
-  rewrite <- Rrepr_plus, <- Rrepr_plus. rewrite Rlt_def in H. exact H.
+  intros. rewrite Rlt_def. apply Rlt_forget. apply (Rplus_lt_reg_r (Rrepr r)).
+  rewrite <- Rrepr_plus, <- Rrepr_plus. rewrite Rlt_def in H.
+  apply Rlt_epsilon. exact H.
 Qed.
 
 Lemma Rplus_le_reg_l : forall r r1 r2, r + r1 <= r + r2 -> r1 <= r2.
@@ -1075,15 +1076,18 @@ Qed.
 Lemma Ropp_gt_lt_contravar : forall r1 r2, r1 > r2 -> - r1 < - r2.
 Proof.
   intros. rewrite Rlt_def. rewrite Rrepr_opp, Rrepr_opp.
+  apply Rlt_forget.
   apply Ropp_gt_lt_contravar. unfold Rgt in H.
-  rewrite Rlt_def in H. exact H.
+  rewrite Rlt_def in H. apply Rlt_epsilon. exact H.
 Qed.
 Hint Resolve Ropp_gt_lt_contravar : core.
 
 Lemma Ropp_lt_gt_contravar : forall r1 r2, r1 < r2 -> - r1 > - r2.
 Proof.
   intros. unfold Rgt. rewrite Rlt_def. rewrite Rrepr_opp, Rrepr_opp.
-  apply Ropp_lt_gt_contravar. rewrite Rlt_def in H. exact H.
+  apply Rlt_forget.
+  apply Ropp_lt_gt_contravar. rewrite Rlt_def in H.
+  apply Rlt_epsilon. exact H.
 Qed.
 Hint Resolve Ropp_lt_gt_contravar: real.
 
@@ -1303,18 +1307,18 @@ Qed.
 
 Lemma Rmult_lt_reg_l : forall r r1 r2, 0 < r -> r * r1 < r * r2 -> r1 < r2.
 Proof.
-  intros. rewrite Rlt_def in H,H0. rewrite Rlt_def.
+  intros. rewrite Rlt_def in H,H0. rewrite Rlt_def. apply Rlt_forget.
   apply (Rmult_lt_reg_l (Rrepr r)).
-  rewrite <- Rrepr_0. exact H.
-  rewrite <- Rrepr_mult, <- Rrepr_mult. exact H0.
+  rewrite <- Rrepr_0. apply Rlt_epsilon. exact H.
+  rewrite <- Rrepr_mult, <- Rrepr_mult. apply Rlt_epsilon. exact H0.
 Qed.
 
 Lemma Rmult_lt_reg_r : forall r r1 r2 : R, 0 < r -> r1 * r < r2 * r -> r1 < r2.
 Proof.
   intros. rewrite Rlt_def. rewrite Rlt_def in H, H0.
-  apply (Rmult_lt_reg_r (Rrepr r)).
-  rewrite <- Rrepr_0. exact H.
-  rewrite <- Rrepr_mult, <- Rrepr_mult. exact H0.
+  apply Rlt_forget. apply (Rmult_lt_reg_r (Rrepr r)).
+  rewrite <- Rrepr_0. apply Rlt_epsilon. exact H.
+  rewrite <- Rrepr_mult, <- Rrepr_mult. apply Rlt_epsilon. exact H0.
 Qed.
 
 Lemma Rmult_gt_reg_l : forall r r1 r2, 0 < r -> r * r1 < r * r2 -> r1 < r2.
@@ -1323,7 +1327,7 @@ Proof. eauto using Rmult_lt_reg_l with rorders. Qed.
 Lemma Rmult_le_reg_l : forall r r1 r2, 0 < r -> r * r1 <= r * r2 -> r1 <= r2.
 Proof.
   intros. rewrite Rrepr_le. rewrite Rlt_def in H. apply (Rmult_le_reg_l (Rrepr r)).
-  rewrite <- Rrepr_0. exact H.
+  rewrite <- Rrepr_0. apply Rlt_epsilon. exact H.
   rewrite <- Rrepr_mult, <- Rrepr_mult.
   rewrite <- Rrepr_le. exact H0.
 Qed.
@@ -1642,7 +1646,7 @@ Hint Resolve pos_INR: real.
 Lemma INR_lt : forall n m:nat, INR n < INR m -> (n < m)%nat.
 Proof.
   intros. apply INR_lt. rewrite Rlt_def in H.
-  rewrite Rrepr_INR, Rrepr_INR in H. exact H.
+  rewrite Rrepr_INR, Rrepr_INR in H. apply Rlt_epsilon. exact H.
 Qed.
 Hint Resolve INR_lt: real.
 
@@ -1676,7 +1680,7 @@ Hint Resolve not_0_INR: real.
 
 Lemma not_INR : forall n m:nat, n <> m -> INR n <> INR m.
 Proof.
-  intros. rewrite Rrepr_appart, Rrepr_INR, Rrepr_INR.
+  intros. apply Rappart_repr. rewrite Rrepr_INR, Rrepr_INR.
   apply not_INR. exact H.
 Qed.
 Hint Resolve not_INR: real.
@@ -1753,8 +1757,8 @@ Proof.
 Qed.
 
 Lemma Rrepr_pow : forall (x : R) (n : nat),
-    (ConstructiveCauchyReals.CRealEq (Rrepr (pow x n))
-                                     (ConstructiveCauchyReals.pow (Rrepr x) n)).
+    (ConstructiveRIneq.Req (Rrepr (pow x n))
+                           (ConstructiveRIneq.pow (Rrepr x) n)).
 Proof.
   intro x. induction n.
   - apply Rrepr_1.
@@ -1801,14 +1805,15 @@ Qed.
 Lemma lt_0_IZR : forall n:Z, 0 < IZR n -> (0 < n)%Z.
 Proof.
   intros. apply lt_0_IZR. rewrite <- Rrepr_0, <- Rrepr_IZR.
-  rewrite Rlt_def in H. exact H.
+  rewrite Rlt_def in H. apply Rlt_epsilon. exact H.
 Qed.
 
 (**********)
 Lemma lt_IZR : forall n m:Z, IZR n < IZR m -> (n < m)%Z.
 Proof.
   intros. apply lt_IZR.
-  rewrite <- Rrepr_IZR, <- Rrepr_IZR. rewrite Rlt_def in H. exact H.
+  rewrite <- Rrepr_IZR, <- Rrepr_IZR. rewrite Rlt_def in H.
+  apply Rlt_epsilon. exact H.
 Qed.
 
 (**********)
@@ -1892,17 +1897,18 @@ Hint Extern 0 (IZR _ <> IZR _) => apply IZR_neq, Zeq_bool_neq, eq_refl : real.
 Lemma one_IZR_lt1 : forall n:Z, -1 < IZR n < 1 -> n = 0%Z.
 Proof.
   intros. apply one_IZR_lt1. do 2 rewrite Rlt_def in H. split.
-  rewrite <- Rrepr_IZR, <- Rrepr_1, <- Rrepr_opp. apply H.
-  rewrite <- Rrepr_IZR, <- Rrepr_1. apply H.
+  rewrite <- Rrepr_IZR, <- Rrepr_1, <- Rrepr_opp.
+  apply Rlt_epsilon. apply H.
+  rewrite <- Rrepr_IZR, <- Rrepr_1. apply Rlt_epsilon. apply H.
 Qed.
 
 Lemma one_IZR_r_R1 :
   forall r (n m:Z), r < IZR n <= r + 1 -> r < IZR m <= r + 1 -> n = m.
 Proof.
   intros. rewrite Rlt_def in H, H0. apply (one_IZR_r_R1 (Rrepr r)); split.
-  rewrite <- Rrepr_IZR. apply H.
+  rewrite <- Rrepr_IZR. apply Rlt_epsilon. apply H.
   rewrite <- Rrepr_IZR, <- Rrepr_1, <- Rrepr_plus, <- Rrepr_le.
-  apply H. rewrite <- Rrepr_IZR. apply H0.
+  apply H. rewrite <- Rrepr_IZR. apply Rlt_epsilon. apply H0.
   rewrite <- Rrepr_IZR, <- Rrepr_1, <- Rrepr_plus, <- Rrepr_le.
   apply H0.
 Qed.
@@ -1939,8 +1945,10 @@ Lemma Rinv_le_contravar :
 Proof.
   intros. apply Rrepr_le. assert (y <> 0).
   intro abs. subst y. apply (Rlt_irrefl 0). exact (Rlt_le_trans 0 x 0 H H0).
-  rewrite Rrepr_appart, Rrepr_0 in H1. rewrite Rlt_def in H. rewrite Rrepr_0 in H.
-  rewrite (Rrepr_inv y H1), (Rrepr_inv x (or_intror H)).
+  apply Rrepr_appart in H1.
+  rewrite Rrepr_0 in H1. rewrite Rlt_def in H. rewrite Rrepr_0 in H.
+  apply Rlt_epsilon in H.
+  rewrite (Rrepr_inv y H1), (Rrepr_inv x (inr H)).
   apply Rinv_le_contravar. rewrite <- Rrepr_le. exact H0.
 Qed.
 
@@ -2008,7 +2016,7 @@ Proof.
   intros. rewrite Rrepr_le. apply le_epsilon.
   intros. rewrite <- (Rquot2 eps), <- Rrepr_plus.
   rewrite <- Rrepr_le. apply H. rewrite Rlt_def.
-  rewrite Rquot2, Rrepr_0. exact H0.
+  rewrite Rquot2, Rrepr_0. apply Rlt_forget. exact H0.
 Qed.
 
 (**********)
diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v
index 8379829037..f03b0ccea3 100644
--- a/theories/Reals/Raxioms.v
+++ b/theories/Reals/Raxioms.v
@@ -8,12 +8,19 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+(* This file continues Rdefinitions, with more properties of the
+   classical reals, including the existence of least upper bounds
+   for non-empty and bounded subsets.
+   The name "Raxioms" and its contents are kept for backward compatibility,
+   when the classical reals were axiomatized. Otherwise we would
+   have merged this file into RIneq. *)
+
 (*********************************************************)
 (**    Lifts of basic operations for classical reals     *)
 (*********************************************************)
 
 Require Export ZArith_base.
-Require Import ConstructiveCauchyReals.
+Require Import ConstructiveRIneq.
 Require Export Rdefinitions.
 Declare Scope R_scope.
 Local Open Scope R_scope.
@@ -26,75 +33,88 @@ Local Open Scope R_scope.
 (** **   Addition                                        *)
 (*********************************************************)
 
-Lemma Rrepr_0 : (Rrepr 0 == 0)%CReal.
+Open Scope R_scope_constr.
+
+Lemma Rrepr_0 : Rrepr 0 == 0.
 Proof.
   intros. unfold IZR. rewrite RbaseSymbolsImpl.R0_def, (Rquot2 0). reflexivity.
 Qed.
 
-Lemma Rrepr_1 : (Rrepr 1 == 1)%CReal.
+Lemma Rrepr_1 : Rrepr 1 == 1.
 Proof.
   intros. unfold IZR, IPR. rewrite RbaseSymbolsImpl.R1_def, (Rquot2 1). reflexivity.
 Qed.
 
-Lemma Rrepr_plus : forall x y:R, (Rrepr (x + y) == Rrepr x + Rrepr y)%CReal.
+Lemma Rrepr_plus : forall x y:R, Rrepr (x + y) == Rrepr x + Rrepr y.
 Proof.
   intros. rewrite RbaseSymbolsImpl.Rplus_def, Rquot2. reflexivity.
 Qed.
 
-Lemma Rrepr_opp : forall x:R, (Rrepr (- x) == - Rrepr x)%CReal.
+Lemma Rrepr_opp : forall x:R, Rrepr (- x) == - Rrepr x.
 Proof.
   intros. rewrite RbaseSymbolsImpl.Ropp_def, Rquot2. reflexivity.
 Qed.
 
-Lemma Rrepr_minus : forall x y:R, (Rrepr (x - y) == Rrepr x - Rrepr y)%CReal.
+Lemma Rrepr_minus : forall x y:R, Rrepr (x - y) == Rrepr x - Rrepr y.
 Proof.
-  intros. unfold Rminus, CReal_minus.
+  intros. unfold Rminus, CRminus.
   rewrite Rrepr_plus, Rrepr_opp. reflexivity.
 Qed.
 
-Lemma Rrepr_mult : forall x y:R, (Rrepr (x * y) == Rrepr x * Rrepr y)%CReal.
+Lemma Rrepr_mult : forall x y:R, Rrepr (x * y) == Rrepr x * Rrepr y.
 Proof.
   intros. rewrite RbaseSymbolsImpl.Rmult_def. rewrite Rquot2. reflexivity.
 Qed.
 
-Lemma Rrepr_inv : forall (x:R) (xnz : (Rrepr x # 0)%CReal),
-    (Rrepr (/ x) == (/ Rrepr x) xnz)%CReal.
+Lemma Rrepr_inv : forall (x:R) (xnz : Rrepr x # 0),
+    Rrepr (/ x) == (/ Rrepr x) xnz.
 Proof.
   intros. rewrite RinvImpl.Rinv_def. destruct (Req_appart_dec x R0).
   - exfalso. subst x. destruct xnz.
-    rewrite Rrepr_0 in H. exact (CRealLt_irrefl 0 H).
-    rewrite Rrepr_0 in H. exact (CRealLt_irrefl 0 H).
-  - rewrite Rquot2. apply (CReal_mult_eq_reg_l (Rrepr x) _ _ xnz).
-    rewrite CReal_mult_comm, (CReal_mult_comm (Rrepr x)), CReal_inv_l, CReal_inv_l.
+    rewrite Rrepr_0 in c. exact (Rlt_irrefl 0 c).
+    rewrite Rrepr_0 in c. exact (Rlt_irrefl 0 c).
+  - rewrite Rquot2. apply (Rmult_eq_reg_l (Rrepr x)). 2: exact xnz.
+    rewrite Rmult_comm, (Rmult_comm (Rrepr x)), Rinv_l, Rinv_l.
     reflexivity.
 Qed.
 
-Lemma Rrepr_le : forall x y:R, x <= y <-> (Rrepr x <= Rrepr y)%CReal.
+Lemma Rrepr_le : forall x y:R, (x <= y)%R <-> Rrepr x <= Rrepr y.
 Proof.
   split.
   - intros [H|H] abs. rewrite RbaseSymbolsImpl.Rlt_def in H.
-    exact (CRealLt_asym (Rrepr x) (Rrepr y) H abs).
-    destruct H. exact (CRealLt_asym (Rrepr x) (Rrepr x) abs abs).
+    apply Rlt_epsilon in H.
+    exact (Rlt_asym (Rrepr x) (Rrepr y) H abs).
+    destruct H. exact (Rlt_asym (Rrepr x) (Rrepr x) abs abs).
   - intros. destruct (total_order_T x y). destruct s.
-    left. exact r. right. exact e. rewrite RbaseSymbolsImpl.Rlt_def in r. contradiction.
+    left. exact r. right. exact e.
+    rewrite RbaseSymbolsImpl.Rlt_def in r. apply Rlt_epsilon in r. contradiction.
 Qed.
 
-Lemma Rrepr_appart : forall x y:R, x <> y <-> (Rrepr x # Rrepr y)%CReal.
+Lemma Rrepr_appart : forall x y:R,
+    (x <> y)%R -> Rrepr x # Rrepr y.
 Proof.
-  split.
-  - intros. destruct (total_order_T x y). destruct s.
-    left. rewrite RbaseSymbolsImpl.Rlt_def in r. exact r. contradiction.
-    right. rewrite RbaseSymbolsImpl.Rlt_def in r. exact r.
-  - intros [H|H] abs.
-    destruct abs. exact (CRealLt_asym (Rrepr x) (Rrepr x) H H).
-    destruct abs. exact (CRealLt_asym (Rrepr x) (Rrepr x) H H).
+  intros. destruct (total_order_T x y). destruct s.
+  left. rewrite RbaseSymbolsImpl.Rlt_def in r.
+  apply Rlt_epsilon. exact r. contradiction.
+  right. rewrite RbaseSymbolsImpl.Rlt_def in r.
+  apply Rlt_epsilon. exact r.
 Qed.
 
+Lemma Rappart_repr : forall x y:R,
+    Rrepr x # Rrepr y -> (x <> y)%R.
+Proof.
+  intros x y [H|H] abs.
+  destruct abs. exact (Rlt_asym (Rrepr x) (Rrepr x) H H).
+  destruct abs. exact (Rlt_asym (Rrepr x) (Rrepr x) H H).
+Qed.
+
+Close Scope R_scope_constr.
+
 
 (**********)
 Lemma Rplus_comm : forall r1 r2:R, r1 + r2 = r2 + r1.
 Proof.
-  intros. apply Rquot1. do 2 rewrite Rrepr_plus. apply CReal_plus_comm.
+  intros. apply Rquot1. do 2 rewrite Rrepr_plus. apply Rplus_comm.
 Qed.
 Hint Resolve Rplus_comm: real.
 
@@ -102,7 +122,7 @@ Hint Resolve Rplus_comm: real.
 Lemma Rplus_assoc : forall r1 r2 r3:R, r1 + r2 + r3 = r1 + (r2 + r3).
 Proof.
   intros. apply Rquot1. repeat rewrite Rrepr_plus.
-  apply CReal_plus_assoc.
+  apply Rplus_assoc.
 Qed.
 Hint Resolve Rplus_assoc: real.
 
@@ -110,7 +130,7 @@ Hint Resolve Rplus_assoc: real.
 Lemma Rplus_opp_r : forall r:R, r + - r = 0.
 Proof.
   intros. apply Rquot1. rewrite Rrepr_plus, Rrepr_opp, Rrepr_0.
-  apply CReal_plus_opp_r.
+  apply Rplus_opp_r.
 Qed.
 Hint Resolve Rplus_opp_r: real.
 
@@ -118,7 +138,7 @@ Hint Resolve Rplus_opp_r: real.
 Lemma Rplus_0_l : forall r:R, 0 + r = r.
 Proof.
   intros. apply Rquot1. rewrite Rrepr_plus, Rrepr_0.
-  apply CReal_plus_0_l.
+  apply Rplus_0_l.
 Qed.
 Hint Resolve Rplus_0_l: real.
 
@@ -129,7 +149,7 @@ Hint Resolve Rplus_0_l: real.
 (**********)
 Lemma Rmult_comm : forall r1 r2:R, r1 * r2 = r2 * r1.
 Proof.
-  intros. apply Rquot1. do 2 rewrite Rrepr_mult. apply CReal_mult_comm.
+  intros. apply Rquot1. do 2 rewrite Rrepr_mult. apply Rmult_comm.
 Qed.
 Hint Resolve Rmult_comm: real.
 
@@ -137,7 +157,7 @@ Hint Resolve Rmult_comm: real.
 Lemma Rmult_assoc : forall r1 r2 r3:R, r1 * r2 * r3 = r1 * (r2 * r3).
 Proof.
   intros. apply Rquot1. repeat rewrite Rrepr_mult.
-  apply CReal_mult_assoc.
+  apply Rmult_assoc.
 Qed.
 Hint Resolve Rmult_assoc: real.
 
@@ -146,7 +166,7 @@ Lemma Rinv_l : forall r:R, r <> 0 -> / r * r = 1.
 Proof.
   intros. rewrite RinvImpl.Rinv_def; destruct (Req_appart_dec r R0).
   - contradiction.
-  - apply Rquot1. rewrite Rrepr_mult, Rquot2, Rrepr_1. apply CReal_inv_l.
+  - apply Rquot1. rewrite Rrepr_mult, Rquot2, Rrepr_1. apply Rinv_l.
 Qed.
 Hint Resolve Rinv_l: real.
 
@@ -154,7 +174,7 @@ Hint Resolve Rinv_l: real.
 Lemma Rmult_1_l : forall r:R, 1 * r = r.
 Proof.
   intros. apply Rquot1. rewrite Rrepr_mult, Rrepr_1.
-  apply CReal_mult_1_l.
+  apply Rmult_1_l.
 Qed.
 Hint Resolve Rmult_1_l: real.
 
@@ -162,16 +182,17 @@ Hint Resolve Rmult_1_l: real.
 Lemma R1_neq_R0 : 1 <> 0.
 Proof.
   intro abs.
-  assert (1 == 0)%CReal.
+  assert (Req (CRone CR) (CRzero CR)).
   { transitivity (Rrepr 1). symmetry.
-    replace 1 with (Rabst 1). 2: unfold IZR,IPR; rewrite RbaseSymbolsImpl.R1_def; reflexivity.
+    replace 1%R with (Rabst (CRone CR)).
+    2: unfold IZR,IPR; rewrite RbaseSymbolsImpl.R1_def; reflexivity.
     rewrite Rquot2. reflexivity. transitivity (Rrepr 0).
     rewrite abs. reflexivity.
-    replace 0 with (Rabst 0).
+    replace 0%R with (Rabst (CRzero CR)).
     2: unfold IZR; rewrite RbaseSymbolsImpl.R0_def; reflexivity.
     rewrite Rquot2. reflexivity. }
-  pose proof (CRealLt_morph 0 0 (CRealEq_refl _) 1 0 H).
-  apply (CRealLt_irrefl 0). apply H0. apply CRealLt_0_1.
+  pose proof (Rlt_morph (CRzero CR) (CRzero CR) (Req_refl _) (CRone CR) (CRzero CR) H).
+  apply (Rlt_irrefl (CRzero CR)). apply H0. apply Rlt_0_1.
 Qed.
 Hint Resolve R1_neq_R0: real.
 
@@ -185,7 +206,7 @@ Lemma
 Proof.
   intros. apply Rquot1.
   rewrite Rrepr_mult, Rrepr_plus, Rrepr_plus, Rrepr_mult, Rrepr_mult.
-  apply CReal_mult_plus_distr_l.
+  apply Rmult_plus_distr_l.
 Qed.
 Hint Resolve Rmult_plus_distr_l: real.
 
@@ -201,30 +222,35 @@ Hint Resolve Rmult_plus_distr_l: real.
 Lemma Rlt_asym : forall r1 r2:R, r1 < r2 -> ~ r2 < r1.
 Proof.
   intros. intro abs. rewrite RbaseSymbolsImpl.Rlt_def in H, abs.
-  apply (CRealLt_asym (Rrepr r1) (Rrepr r2)); assumption.
+  apply Rlt_epsilon in H. apply Rlt_epsilon in abs.
+  apply (Rlt_asym (Rrepr r1) (Rrepr r2)); assumption.
 Qed.
 
 (**********)
 Lemma Rlt_trans : forall r1 r2 r3:R, r1 < r2 -> r2 < r3 -> r1 < r3.
 Proof.
   intros. rewrite RbaseSymbolsImpl.Rlt_def. rewrite RbaseSymbolsImpl.Rlt_def in H, H0.
-  apply (CRealLt_trans (Rrepr r1) (Rrepr r2) (Rrepr r3)); assumption.
+  apply Rlt_epsilon in H. apply Rlt_epsilon in H0.
+  apply Rlt_forget.
+  apply (Rlt_trans (Rrepr r1) (Rrepr r2) (Rrepr r3)); assumption.
 Qed.
 
 (**********)
 Lemma Rplus_lt_compat_l : forall r r1 r2:R, r1 < r2 -> r + r1 < r + r2.
 Proof.
   intros. rewrite RbaseSymbolsImpl.Rlt_def. rewrite RbaseSymbolsImpl.Rlt_def in H.
-  do 2 rewrite Rrepr_plus. apply CReal_plus_lt_compat_l. exact H.
+  do 2 rewrite Rrepr_plus. apply Rlt_forget.
+  apply Rplus_lt_compat_l. apply Rlt_epsilon. exact H.
 Qed.
 
 (**********)
 Lemma Rmult_lt_compat_l : forall r r1 r2:R, 0 < r -> r1 < r2 -> r * r1 < r * r2.
 Proof.
   intros. rewrite RbaseSymbolsImpl.Rlt_def. rewrite RbaseSymbolsImpl.Rlt_def in H.
-  do 2 rewrite Rrepr_mult. apply CReal_mult_lt_compat_l.
-  rewrite <- (Rquot2 0). unfold IZR in H. rewrite RbaseSymbolsImpl.R0_def in H. exact H.
-  rewrite RbaseSymbolsImpl.Rlt_def in H0. exact H0.
+  do 2 rewrite Rrepr_mult. apply Rlt_forget. apply Rmult_lt_compat_l.
+  rewrite <- (Rquot2 (CRzero CR)). unfold IZR in H.
+  rewrite RbaseSymbolsImpl.R0_def in H. apply Rlt_epsilon. exact H.
+  rewrite RbaseSymbolsImpl.Rlt_def in H0. apply Rlt_epsilon. exact H0.
 Qed.
 
 Hint Resolve Rlt_asym Rplus_lt_compat_l Rmult_lt_compat_l: real.
@@ -247,7 +273,7 @@ Arguments INR n%nat.
 (**********************************************************)
 
 Lemma Rrepr_INR : forall n : nat,
-    (Rrepr (INR n) == ConstructiveCauchyReals.INR n)%CReal.
+    Req (Rrepr (INR n)) (ConstructiveRIneq.INR n).
 Proof.
   induction n.
   - apply Rrepr_0.
@@ -256,41 +282,41 @@ Proof.
 Qed.
 
 Lemma Rrepr_IPR2 : forall n : positive,
-    (Rrepr (IPR_2 n) == ConstructiveCauchyReals.IPR_2 n)%CReal.
+    Req (Rrepr (IPR_2 n)) (ConstructiveRIneq.IPR_2 n).
 Proof.
   induction n.
-  - unfold IPR_2, ConstructiveCauchyReals.IPR_2.
+  - unfold IPR_2, ConstructiveRIneq.IPR_2.
     rewrite RbaseSymbolsImpl.R1_def, Rrepr_mult, Rrepr_plus, Rrepr_plus, <- IHn.
     unfold IPR_2.
     rewrite Rquot2. rewrite RbaseSymbolsImpl.R1_def. reflexivity.
-  - unfold IPR_2, ConstructiveCauchyReals.IPR_2.
+  - unfold IPR_2, ConstructiveRIneq.IPR_2.
     rewrite Rrepr_mult, Rrepr_plus, <- IHn.
     rewrite RbaseSymbolsImpl.R1_def. rewrite Rquot2.
     unfold IPR_2. rewrite RbaseSymbolsImpl.R1_def. reflexivity.
-  - unfold IPR_2, ConstructiveCauchyReals.IPR_2.
+  - unfold IPR_2, ConstructiveRIneq.IPR_2.
     rewrite RbaseSymbolsImpl.R1_def.
     rewrite Rrepr_plus, Rquot2. reflexivity.
 Qed.
 
 Lemma Rrepr_IPR : forall n : positive,
-    (Rrepr (IPR n) == ConstructiveCauchyReals.IPR n)%CReal.
+    Req (Rrepr (IPR n)) (ConstructiveRIneq.IPR n).
 Proof.
   intro n. destruct n.
-  - unfold IPR, ConstructiveCauchyReals.IPR.
+  - unfold IPR, ConstructiveRIneq.IPR.
     rewrite Rrepr_plus, <- Rrepr_IPR2.
     rewrite RbaseSymbolsImpl.R1_def. rewrite Rquot2. reflexivity.
-  - unfold IPR, ConstructiveCauchyReals.IPR.
+  - unfold IPR, ConstructiveRIneq.IPR.
     apply Rrepr_IPR2.
   - unfold IPR. rewrite RbaseSymbolsImpl.R1_def. apply Rquot2.
 Qed.
 
 Lemma Rrepr_IZR : forall n : Z,
-    (Rrepr (IZR n) == ConstructiveCauchyReals.IZR n)%CReal.
+    Req (Rrepr (IZR n)) (ConstructiveRIneq.IZR n).
 Proof.
   intros [|p|n].
   - unfold IZR. rewrite RbaseSymbolsImpl.R0_def. apply Rquot2.
   - apply Rrepr_IPR.
-  - unfold IZR, ConstructiveCauchyReals.IZR.
+  - unfold IZR, ConstructiveRIneq.IZR.
     rewrite <- Rrepr_IPR, Rrepr_opp. reflexivity.
 Qed.
 
@@ -300,38 +326,66 @@ Proof.
   intro r. unfold up.
   destruct (Rarchimedean (Rrepr r)) as [n nmaj], (total_order_T (IZR n - r) R1).
   destruct s.
-  - split. unfold Rgt. rewrite RbaseSymbolsImpl.Rlt_def. rewrite Rrepr_IZR. apply nmaj.
+  - split. unfold Rgt. rewrite RbaseSymbolsImpl.Rlt_def. rewrite Rrepr_IZR.
+    apply Rlt_forget. apply nmaj.
     unfold Rle. left. exact r0.
-  - split. unfold Rgt. rewrite RbaseSymbolsImpl.Rlt_def. rewrite Rrepr_IZR. apply nmaj.
-    right. exact e.
+  - split. unfold Rgt. rewrite RbaseSymbolsImpl.Rlt_def.
+    rewrite Rrepr_IZR. apply Rlt_forget. apply nmaj. right. exact e.
   - split.
-    + unfold Rgt, Z.pred. rewrite RbaseSymbolsImpl.Rlt_def. rewrite Rrepr_IZR, plus_IZR.
+    + unfold Rgt, Z.pred. rewrite RbaseSymbolsImpl.Rlt_def.
+      rewrite Rrepr_IZR, plus_IZR.
       rewrite RbaseSymbolsImpl.Rlt_def in r0. rewrite Rrepr_minus in r0.
       rewrite <- (Rrepr_IZR n).
-      unfold ConstructiveCauchyReals.IZR, ConstructiveCauchyReals.IPR.
-      apply (CReal_plus_lt_compat_l (Rrepr r - Rrepr R1)) in r0.
-      ring_simplify in r0. rewrite RbaseSymbolsImpl.R1_def in r0. rewrite Rquot2 in r0.
-      rewrite CReal_plus_comm. exact r0.
+      unfold ConstructiveRIneq.IZR, ConstructiveRIneq.IPR.
+      apply Rlt_forget. apply Rlt_epsilon in r0.
+      unfold ConstructiveRIneq.Rminus in r0.
+      apply (ConstructiveRIneq.Rplus_lt_compat_l
+               (ConstructiveRIneq.Rplus (Rrepr r) (ConstructiveRIneq.Ropp (Rrepr R1))))
+        in r0.
+      rewrite ConstructiveRIneq.Rplus_assoc,
+      ConstructiveRIneq.Rplus_opp_l,
+      ConstructiveRIneq.Rplus_0_r,
+      RbaseSymbolsImpl.R1_def, Rquot2,
+      ConstructiveRIneq.Rplus_comm,
+      ConstructiveRIneq.Rplus_assoc,
+      <- (ConstructiveRIneq.Rplus_assoc (ConstructiveRIneq.Ropp (Rrepr r))),
+      ConstructiveRIneq.Rplus_opp_l,
+      ConstructiveRIneq.Rplus_0_l
+        in r0.
+      exact r0.
     + destruct (total_order_T (IZR (Z.pred n) - r) 1). destruct s.
       left. exact r1. right. exact e.
-      exfalso. rewrite <- Rrepr_IZR in nmaj.
+      exfalso. destruct nmaj as [_ nmaj]. rewrite <- Rrepr_IZR in nmaj.
       apply (Rlt_asym (IZR n) (r + 2)).
       rewrite RbaseSymbolsImpl.Rlt_def. rewrite Rrepr_plus. rewrite (Rrepr_plus 1 1).
-      apply (CRealLt_Le_trans _ (Rrepr r + 2)). apply nmaj.
-      unfold IZR, IPR. rewrite RbaseSymbolsImpl.R1_def, Rquot2. apply CRealLe_refl.
+      apply Rlt_forget.
+      apply (ConstructiveRIneq.Rlt_le_trans
+               _ (ConstructiveRIneq.Rplus (Rrepr r) (ConstructiveRIneq.IZR 2))).
+      apply nmaj.
+      unfold IZR, IPR. rewrite RbaseSymbolsImpl.R1_def, Rquot2. apply Rle_refl.
       clear nmaj.
       unfold Z.pred in r1. rewrite RbaseSymbolsImpl.Rlt_def in r1.
       rewrite Rrepr_minus, (Rrepr_IZR (n + -1)), plus_IZR,
       <- (Rrepr_IZR n)
         in r1.
-      unfold ConstructiveCauchyReals.IZR, ConstructiveCauchyReals.IPR in r1.
+      unfold ConstructiveRIneq.IZR, ConstructiveRIneq.IPR in r1.
       rewrite RbaseSymbolsImpl.Rlt_def, Rrepr_plus.
-      apply (CReal_plus_lt_compat_l (Rrepr r + 1)) in r1.
-      ring_simplify in r1.
-      apply (CRealLe_Lt_trans _ (Rrepr r + Rrepr 1 + 1)). 2: apply r1.
+      apply Rlt_epsilon in r1.
+      apply (ConstructiveRIneq.Rplus_lt_compat_l
+               (ConstructiveRIneq.Rplus (Rrepr r) (CRone CR))) in r1.
+      apply Rlt_forget.
+      apply (ConstructiveRIneq.Rle_lt_trans
+               _ (ConstructiveRIneq.Rplus (ConstructiveRIneq.Rplus (Rrepr r) (Rrepr 1)) (CRone CR))).
       rewrite (Rrepr_plus 1 1). unfold IZR, IPR.
-      rewrite RbaseSymbolsImpl.R1_def, (Rquot2 1), <- CReal_plus_assoc.
-      apply CRealLe_refl.
+      rewrite RbaseSymbolsImpl.R1_def, (Rquot2 (CRone CR)), <- ConstructiveRIneq.Rplus_assoc.
+      apply Rle_refl.
+      rewrite <- (ConstructiveRIneq.Rplus_comm (Rrepr 1)),
+      <- ConstructiveRIneq.Rplus_assoc,
+      (ConstructiveRIneq.Rplus_comm (Rrepr 1))
+        in r1.
+      apply (ConstructiveRIneq.Rlt_le_trans _ _ _ r1).
+      unfold ConstructiveRIneq.Rminus.
+      ring_simplify. apply ConstructiveRIneq.Rle_refl.
 Qed.
 
 (**********************************************************)
@@ -349,12 +403,30 @@ 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:ConstructiveRIneq.R => E (Rabst x)) as Er.
+  assert (exists x : ConstructiveRIneq.R, 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 : ConstructiveRIneq.R,
+             (forall y:ConstructiveRIneq.R, Er y -> ConstructiveRIneq.Rle y x))
+    as Ebound.
+  { destruct H. exists (Rrepr x). intros y Ey. rewrite <- (Rquot2 y).
+    apply Rrepr_le. apply H. exact Ey. }
+  destruct (CR_sig_lub CR
+              Er sig_forall_dec sig_not_dec Einhab Ebound).
+  exists (Rabst x). split.
+  intros y Ey. apply Rrepr_le. rewrite Rquot2.
+  unfold ConstructiveRIneq.Rle. apply a.
+  unfold Er. replace (Rabst (Rrepr y)) with y. exact Ey.
+  apply Rquot1. rewrite Rquot2. reflexivity.
+  intros. destruct a. apply Rrepr_le. rewrite Rquot2.
+  unfold ConstructiveRIneq.Rle. apply H3. intros y Ey.
+  intros. rewrite <- (Rquot2 y) in H4.
+  apply Rrepr_le in H4. exact H4.
+  apply H1, Ey.
+Qed.
diff --git a/theories/Reals/Rdefinitions.v b/theories/Reals/Rdefinitions.v
index 03eb6c8b44..b1ce8109ca 100644
--- a/theories/Reals/Rdefinitions.v
+++ b/theories/Reals/Rdefinitions.v
@@ -8,11 +8,15 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-(* Classical quotient of the constructive Cauchy real numbers. *)
+(* Classical quotient of the constructive Cauchy real numbers.
+   This file contains the definition of the classical real numbers
+   type R, its algebraic operations, its order and the proof that
+   it is total, and the proof that R is archimedean (up).
+   It also defines IZR, the ring morphism from Z to R. *)
 
 Require Export ZArith_base.
 Require Import QArith_base.
-Require Import ConstructiveCauchyReals.
+Require Import ConstructiveRIneq.
 
 Parameter R : Set.
 
@@ -30,13 +34,16 @@ Local Open Scope R_scope.
 
 (* The limited principle of omniscience *)
 Axiom sig_forall_dec
-  : forall (P : nat -> Prop), (forall n, {P n} + {~P n})
-                   -> {n | ~P n} + {forall n, P n}.
+  : forall (P : nat -> Prop),
+    (forall n, {P n} + {~P n})
+    -> {n | ~P n} + {forall n, P n}.
 
-Axiom Rabst : CReal -> R.
-Axiom Rrepr : R -> CReal.
-Axiom Rquot1 : forall x y:R, CRealEq (Rrepr x) (Rrepr y) -> x = y.
-Axiom Rquot2 : forall x:CReal, CRealEq (Rrepr (Rabst x)) x.
+Axiom sig_not_dec : forall P : Prop, { ~~P } + { ~P }.
+
+Axiom Rabst : ConstructiveRIneq.R -> R.
+Axiom Rrepr : R -> ConstructiveRIneq.R.
+Axiom Rquot1 : forall x y:R, Req (Rrepr x) (Rrepr y) -> x = y.
+Axiom Rquot2 : forall x:ConstructiveRIneq.R, Req (Rrepr (Rabst x)) x.
 
 (* Those symbols must be kept opaque, for backward compatibility. *)
 Module Type RbaseSymbolsSig.
@@ -47,29 +54,29 @@ Module Type RbaseSymbolsSig.
   Parameter Ropp : R -> R.
   Parameter Rlt : R -> R -> Prop.
 
-  Parameter R0_def : R0 = Rabst 0%CReal.
-  Parameter R1_def : R1 = Rabst 1%CReal.
+  Parameter R0_def : R0 = Rabst (CRzero CR).
+  Parameter R1_def : R1 = Rabst (CRone CR).
   Parameter Rplus_def : forall x y : R,
-      Rplus x y = Rabst (CReal_plus (Rrepr x) (Rrepr y)).
+      Rplus x y = Rabst (ConstructiveRIneq.Rplus (Rrepr x) (Rrepr y)).
   Parameter Rmult_def : forall x y : R,
-      Rmult x y = Rabst (CReal_mult (Rrepr x) (Rrepr y)).
+      Rmult x y = Rabst (ConstructiveRIneq.Rmult (Rrepr x) (Rrepr y)).
   Parameter Ropp_def : forall x : R,
-      Ropp x = Rabst (CReal_opp (Rrepr x)).
+      Ropp x = Rabst (ConstructiveRIneq.Ropp (Rrepr x)).
   Parameter Rlt_def : forall x y : R,
-      Rlt x y = CRealLt (Rrepr x) (Rrepr y).
+      Rlt x y = ConstructiveRIneq.RltProp (Rrepr x) (Rrepr y).
 End RbaseSymbolsSig.
 
 Module RbaseSymbolsImpl : RbaseSymbolsSig.
-  Definition R0 : R := Rabst 0%CReal.
-  Definition R1 : R := Rabst 1%CReal.
+  Definition R0 : R := Rabst (CRzero CR).
+  Definition R1 : R := Rabst (CRone CR).
   Definition Rplus : R -> R -> R
-    := fun x y : R => Rabst (CReal_plus (Rrepr x) (Rrepr y)).
+    := fun x y : R => Rabst (ConstructiveRIneq.Rplus (Rrepr x) (Rrepr y)).
   Definition Rmult : R -> R -> R
-    := fun x y : R => Rabst (CReal_mult (Rrepr x) (Rrepr y)).
+    := fun x y : R => Rabst (ConstructiveRIneq.Rmult (Rrepr x) (Rrepr y)).
   Definition Ropp : R -> R
-    := fun x : R => Rabst (CReal_opp (Rrepr x)).
+    := fun x : R => Rabst (ConstructiveRIneq.Ropp (Rrepr x)).
   Definition Rlt : R -> R -> Prop
-    := fun x y : R => CRealLt (Rrepr x) (Rrepr y).
+    := fun x y : R => ConstructiveRIneq.RltProp (Rrepr x) (Rrepr y).
 
   Definition R0_def := eq_refl R0.
   Definition R1_def := eq_refl R1.
@@ -151,31 +158,13 @@ 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)).
-  - left. left. rewrite RbaseSymbolsImpl.Rlt_def. exact c.
-  - destruct (CRealLt_dec (Rrepr r2) (Rrepr r1)).
-    + right. rewrite RbaseSymbolsImpl.Rlt_def. exact c.
+  intros. destruct (Rlt_lpo_dec (Rrepr r1) (Rrepr r2) sig_forall_dec).
+  - left. left. rewrite RbaseSymbolsImpl.Rlt_def.
+    apply Rlt_forget. exact r.
+  - destruct (Rlt_lpo_dec (Rrepr r2) (Rrepr r1) sig_forall_dec).
+    + right. rewrite RbaseSymbolsImpl.Rlt_def. apply Rlt_forget. exact r0.
     + left. right. apply Rquot1. split; assumption.
 Qed.
 
@@ -189,10 +178,13 @@ Proof.
 Qed.
 
 Lemma Rrepr_appart_0 : forall x:R,
-    (x < R0 \/ R0 < x) -> (Rrepr x # 0)%CReal.
+    (x < R0 \/ R0 < x) -> Rappart (Rrepr x) (CRzero CR).
 Proof.
-  intros. destruct H. left. rewrite RbaseSymbolsImpl.Rlt_def, RbaseSymbolsImpl.R0_def, Rquot2 in H. exact H.
-  right. rewrite RbaseSymbolsImpl.Rlt_def, RbaseSymbolsImpl.R0_def, Rquot2 in H. exact H.
+  intros. apply CRltDisjunctEpsilon. destruct H.
+  left. rewrite RbaseSymbolsImpl.Rlt_def, RbaseSymbolsImpl.R0_def, Rquot2 in H.
+  exact H.
+  right. rewrite RbaseSymbolsImpl.Rlt_def, RbaseSymbolsImpl.R0_def, Rquot2 in H.
+  exact H.
 Qed.
 
 Module Type RinvSig.
@@ -200,7 +192,7 @@ Module Type RinvSig.
   Parameter Rinv_def : forall x : R,
       Rinv x = match Req_appart_dec x R0 with
                | left _ => R0 (* / 0 is undefined, we take 0 arbitrarily *)
-               | right r => Rabst ((CReal_inv (Rrepr x) (Rrepr_appart_0 x r)))
+               | right r => Rabst ((ConstructiveRIneq.Rinv (Rrepr x) (Rrepr_appart_0 x r)))
                end.
 End RinvSig.
 
@@ -208,7 +200,7 @@ Module RinvImpl : RinvSig.
   Definition Rinv : R -> R
     := fun x => match Req_appart_dec x R0 with
              | left _ => R0 (* / 0 is undefined, we take 0 arbitrarily *)
-             | right r => Rabst ((CReal_inv (Rrepr x) (Rrepr_appart_0 x r)))
+             | right r => Rabst ((ConstructiveRIneq.Rinv (Rrepr x) (Rrepr_appart_0 x r)))
              end.
   Definition Rinv_def := fun x => eq_refl (Rinv x).
 End RinvImpl.