Merge PR #12287: Define CRzero and CRone via CR_of_Q

Reviewed-by: MSoegtropIMC

7 files changed, 229 insertions, 251 deletions

diff --git a/theories/Reals/Abstract/ConstructiveAbs.v b/theories/Reals/Abstract/ConstructiveAbs.v
index d357ad2d54..31397cbddd 100644
--- a/theories/Reals/Abstract/ConstructiveAbs.v
+++ b/theories/Reals/Abstract/ConstructiveAbs.v
@@ -57,11 +57,11 @@ Proof.
   - pose proof (CRabs_def R x (CRabs R x)) as [_ H1].
     apply H1, CRle_refl.
   - rewrite <- CRabs_def. split. apply CRle_refl.
-    apply (CRle_trans _ (CRzero R)). 2: exact H.
-    apply (CRle_trans _ (CRopp R (CRzero R))).
+    apply (CRle_trans _ 0). 2: exact H.
+    apply (CRle_trans _ (CRopp R 0)).
     intro abs. apply CRopp_lt_cancel in abs. contradiction.
-    apply (CRplus_le_reg_l (CRzero R)).
-    apply (CRle_trans _ (CRzero R)). apply CRplus_opp_r.
+    apply (CRplus_le_reg_l 0).
+    apply (CRle_trans _ 0). apply CRplus_opp_r.
     apply CRplus_0_r.
 Qed.
 
@@ -164,8 +164,7 @@ Lemma CR_of_Q_abs : forall {R : ConstructiveReals} (q : Q),
 Proof.
   intros. destruct (Qlt_le_dec 0 q).
   - apply (CReq_trans _ (CR_of_Q R q)).
-    apply CRabs_right. apply (CRle_trans _ (CR_of_Q R 0)).
-    apply CR_of_Q_zero. apply CR_of_Q_le. apply Qlt_le_weak, q0.
+    apply CRabs_right. apply CR_of_Q_le. apply Qlt_le_weak, q0.
     apply CR_of_Q_morph. symmetry. apply Qabs_pos, Qlt_le_weak, q0.
   - apply (CReq_trans _ (CR_of_Q R (-q))).
     apply (CReq_trans _ (CRabs R (CRopp R (CR_of_Q R q)))).
@@ -173,8 +172,7 @@ Proof.
     2: apply CR_of_Q_morph; symmetry; apply Qabs_neg, q0.
     apply (CReq_trans _ (CRopp R (CR_of_Q R q))).
     2: apply CReq_sym, CR_of_Q_opp.
-    apply CRabs_right. apply (CRle_trans _ (CR_of_Q R 0)).
-    apply CR_of_Q_zero.
+    apply CRabs_right.
     apply (CRle_trans _ (CR_of_Q R (-q))). apply CR_of_Q_le.
     apply (Qplus_le_l _ _ q). ring_simplify. exact q0.
     apply CR_of_Q_opp.
@@ -206,14 +204,14 @@ Proof.
   destruct (CR_Q_dense R _ _ neg) as [q [H0 H1]].
   destruct (Qlt_le_dec 0 q).
   - destruct (s (CR_of_Q R (-q)) x 0).
-    rewrite <- CR_of_Q_zero. apply CR_of_Q_lt.
+    apply CR_of_Q_lt.
     apply (Qplus_lt_l _ _ q). ring_simplify. exact q0.
     exfalso. pose proof (CRabs_def R x (CR_of_Q R q)) as [H2 _].
     apply H2. clear H2. split. apply CRlt_asym, H0.
     2: exact H1. rewrite <- Qopp_involutive, CR_of_Q_opp.
     apply CRopp_ge_le_contravar, CRlt_asym, c. exact c.
   - apply (CRlt_le_trans _ _ _ H0).
-    rewrite <- CR_of_Q_zero. apply CR_of_Q_le. exact q0.
+    apply CR_of_Q_le. exact q0.
 Qed.
 
 
@@ -339,24 +337,23 @@ Proof.
   left; apply CR_of_Q_pos; reflexivity.
   rewrite CRmult_assoc, <- CR_of_Q_mult.
   setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity.
-  rewrite CR_of_Q_one, CRmult_1_r.
-  rewrite (CR_of_Q_plus R 1 1), CR_of_Q_one, CRmult_plus_distr_l, CRmult_1_r.
+  rewrite CRmult_1_r.
+  rewrite (CR_of_Q_plus R 1 1), CRmult_plus_distr_l, CRmult_1_r.
   rewrite CRabs_right. unfold CRminus.
   rewrite CRopp_plus_distr, CRplus_assoc, <- (CRplus_assoc y).
   rewrite CRplus_opp_r, CRplus_0_l, CRopp_involutive. reflexivity.
   apply (CRmult_lt_compat_r (CR_of_Q R 2)) in H.
   2: apply CR_of_Q_pos; reflexivity.
-  rewrite CRmult_assoc, <- CR_of_Q_mult in H.
-  setoid_replace ((1 # 2) * 2)%Q with 1%Q in H. 2: reflexivity.
-  rewrite CR_of_Q_one, CRmult_1_r in H.
-  rewrite CRmult_comm, (CR_of_Q_plus R 1 1), CR_of_Q_one, CRmult_plus_distr_r,
-  CRmult_1_l in H.
-  intro abs. rewrite CRabs_left in H.
-  unfold CRminus in H.
-  rewrite CRopp_involutive, CRplus_comm in H.
-  rewrite CRplus_assoc, <- (CRplus_assoc (-x)), CRplus_opp_l in H.
-  rewrite CRplus_0_l in H. exact (CRlt_asym _ _ H H).
-  apply CRlt_asym, abs.
+  intro abs. contradict H.
+  apply (CRle_trans _ (x + y - CRabs R (y - x))).
+  rewrite CRabs_left. 2: apply CRlt_asym, abs.
+  unfold CRminus. rewrite CRopp_involutive, CRplus_comm.
+  rewrite CRplus_assoc, <- (CRplus_assoc (-x)), CRplus_opp_l.
+  rewrite CRplus_0_l, (CR_of_Q_plus R 1 1), CRmult_plus_distr_l.
+  rewrite CRmult_1_r. apply CRle_refl.
+  rewrite CRmult_assoc, <- CR_of_Q_mult.
+  setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity.
+  rewrite CRmult_1_r. apply CRle_refl.
 Qed.
 
 Add Parametric Morphism {R : ConstructiveReals} : CRmin
@@ -383,11 +380,11 @@ Lemma CRmin_l : forall {R : ConstructiveReals} (x y : CRcarrier R),
 Proof.
   intros. unfold CRmin.
   apply (CRmult_le_reg_r (CR_of_Q R 2)).
-  rewrite <- CR_of_Q_zero. apply CR_of_Q_lt; reflexivity.
+  apply CR_of_Q_lt; reflexivity.
   rewrite CRmult_assoc, <- CR_of_Q_mult.
   setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity.
-  rewrite CR_of_Q_one, CRmult_1_r.
-  rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CR_of_Q_one, CRmult_1_r.
+  rewrite CRmult_1_r.
+  rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CRmult_1_r.
   unfold CRminus. rewrite CRplus_assoc. apply CRplus_le_compat_l.
   apply (CRplus_le_reg_r (CRabs _ (y + - x)+ -x)).
   rewrite CRplus_assoc, <- (CRplus_assoc (-CRabs _ (y + - x))).
@@ -401,11 +398,11 @@ Lemma CRmin_r : forall {R : ConstructiveReals} (x y : CRcarrier R),
 Proof.
   intros. unfold CRmin.
   apply (CRmult_le_reg_r (CR_of_Q R 2)).
-  rewrite <- CR_of_Q_zero. apply CR_of_Q_lt; reflexivity.
+  apply CR_of_Q_lt; reflexivity.
   rewrite CRmult_assoc, <- CR_of_Q_mult.
   setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity.
-  rewrite CR_of_Q_one, CRmult_1_r.
-  rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CR_of_Q_one, CRmult_1_r.
+  rewrite CRmult_1_r.
+  rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CRmult_1_r.
   rewrite (CRplus_comm x).
   unfold CRminus. rewrite CRplus_assoc. apply CRplus_le_compat_l.
   apply (CRplus_le_reg_l (-x)).
@@ -451,15 +448,15 @@ Proof.
   intros. unfold CRmin.
   unfold CRminus. setoid_replace (x + z + - (x + y)) with (z-y).
   apply (CRmult_eq_reg_r (CR_of_Q _ 2)).
-  left. rewrite <- CR_of_Q_zero. apply CR_of_Q_lt; reflexivity.
+  left. apply CR_of_Q_lt; reflexivity.
   rewrite CRmult_plus_distr_r.
   rewrite CRmult_assoc, <- CR_of_Q_mult.
   setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity.
-  rewrite CR_of_Q_one, CRmult_1_r.
+  rewrite CRmult_1_r.
   rewrite CRmult_assoc, <- CR_of_Q_mult.
   setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity.
-  rewrite CR_of_Q_one, CRmult_1_r.
-  rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CR_of_Q_one, CRmult_1_r.
+  rewrite CRmult_1_r.
+  rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CRmult_1_r.
   do 3 rewrite (CRplus_assoc x). apply CRplus_morph. reflexivity.
   do 2 rewrite <- CRplus_assoc. apply CRplus_morph. 2: reflexivity.
   rewrite (CRplus_comm x). apply CRplus_assoc.
@@ -474,11 +471,11 @@ Lemma CRmin_left : forall {R : ConstructiveReals} (x y : CRcarrier R),
 Proof.
   intros. unfold CRmin.
   apply (CRmult_eq_reg_r (CR_of_Q R 2)).
-  left. rewrite <- CR_of_Q_zero. apply CR_of_Q_lt; reflexivity.
+  left. apply CR_of_Q_lt; reflexivity.
   rewrite CRmult_assoc, <- CR_of_Q_mult.
   setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity.
-  rewrite CR_of_Q_one, CRmult_1_r.
-  rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CR_of_Q_one, CRmult_1_r.
+  rewrite CRmult_1_r.
+  rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CRmult_1_r.
   rewrite CRabs_right. unfold CRminus. rewrite CRopp_plus_distr.
   rewrite CRplus_assoc. apply CRplus_morph. reflexivity.
   rewrite <- CRplus_assoc, CRplus_opp_r, CRplus_0_l. apply CRopp_involutive.
@@ -491,11 +488,11 @@ Lemma CRmin_right : forall {R : ConstructiveReals} (x y : CRcarrier R),
 Proof.
   intros. unfold CRmin.
   apply (CRmult_eq_reg_r (CR_of_Q R 2)).
-  left. rewrite <- CR_of_Q_zero. apply CR_of_Q_lt; reflexivity.
+  left. apply CR_of_Q_lt; reflexivity.
   rewrite CRmult_assoc, <- CR_of_Q_mult.
   setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity.
-  rewrite CR_of_Q_one, CRmult_1_r.
-  rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CR_of_Q_one, CRmult_1_r.
+  rewrite CRmult_1_r.
+  rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CRmult_1_r.
   rewrite CRabs_left. unfold CRminus. do 2 rewrite CRopp_plus_distr.
   rewrite (CRplus_comm x y).
   rewrite CRplus_assoc. apply CRplus_morph. reflexivity.
@@ -510,10 +507,10 @@ Lemma CRmin_lt : forall {R : ConstructiveReals} (x y z : CRcarrier R),
 Proof.
   intros. unfold CRmin.
   apply (CRmult_lt_reg_r (CR_of_Q R 2)).
-  rewrite <- CR_of_Q_zero. apply CR_of_Q_lt; reflexivity.
+  apply CR_of_Q_lt; reflexivity.
   rewrite CRmult_assoc, <- CR_of_Q_mult.
   setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity.
-  rewrite CR_of_Q_one, CRmult_1_r.
+  rewrite CRmult_1_r.
   apply (CRplus_lt_reg_l _ (CRabs _ (y - x) - (z*CR_of_Q R 2))).
   unfold CRminus. rewrite CRplus_assoc. rewrite CRplus_opp_l, CRplus_0_r.
   rewrite (CRplus_comm (CRabs R (y + - x))).
@@ -526,7 +523,7 @@ Proof.
     apply (CRplus_lt_reg_l R (-x)).
     rewrite CRopp_mult_distr_l.
     rewrite <- CRplus_assoc, CRplus_opp_l, CRplus_0_l.
-    rewrite (CR_of_Q_plus R 1 1), CR_of_Q_one, CRmult_plus_distr_l.
+    rewrite (CR_of_Q_plus R 1 1), CRmult_plus_distr_l.
     rewrite CRmult_1_r. apply CRplus_le_lt_compat.
     apply CRlt_asym.
     apply CRopp_gt_lt_contravar, H.
@@ -537,7 +534,7 @@ Proof.
     apply (CRplus_lt_reg_l R (-y)).
     rewrite CRopp_mult_distr_l.
     rewrite <- CRplus_assoc, CRplus_opp_l, CRplus_0_l.
-    rewrite (CR_of_Q_plus R 1 1), CR_of_Q_one, CRmult_plus_distr_l.
+    rewrite (CR_of_Q_plus R 1 1), CRmult_plus_distr_l.
     rewrite CRmult_1_r. apply CRplus_le_lt_compat.
     apply CRlt_asym.
     apply CRopp_gt_lt_contravar, H0.
@@ -552,12 +549,12 @@ Proof.
   rewrite (CRabs_morph
              _ ((x - y + (CRabs _ (a - y) - CRabs _ (a - x))) * CR_of_Q R (1 # 2))).
   rewrite CRabs_mult, (CRabs_right (CR_of_Q R (1 # 2))).
-  2: rewrite <- CR_of_Q_zero; apply CR_of_Q_le; discriminate.
+  2: apply CR_of_Q_le; discriminate.
   apply (CRle_trans _
            ((CRabs _ (x - y) * 1 + CRabs _ (x-y) * 1)
               * CR_of_Q R (1 # 2))).
   apply CRmult_le_compat_r.
-  rewrite <- CR_of_Q_zero. apply CR_of_Q_le. discriminate.
+  apply CR_of_Q_le. discriminate.
   apply (CRle_trans
            _ (CRabs _ (x - y) + CRabs _ (CRabs _ (a - y) - CRabs _ (a - x)))).
   apply CRabs_triang. rewrite CRmult_1_r. apply CRplus_le_compat_l.
@@ -568,11 +565,11 @@ Proof.
   rewrite CRplus_comm, CRopp_plus_distr, <- CRplus_assoc.
   rewrite CRplus_opp_r, CRopp_involutive, CRplus_0_l.
   reflexivity.
-  rewrite <- CRmult_plus_distr_l, <- CR_of_Q_one.
+  rewrite <- CRmult_plus_distr_l.
   rewrite <- (CR_of_Q_plus R 1 1).
   rewrite CRmult_assoc, <- CR_of_Q_mult.
   setoid_replace ((1 + 1) * (1 # 2))%Q with 1%Q. 2: reflexivity.
-  rewrite CR_of_Q_one, CRmult_1_r. apply CRle_refl.
+  rewrite CRmult_1_r. apply CRle_refl.
   unfold CRminus. apply CRmult_morph. 2: reflexivity.
   do 4 rewrite CRplus_assoc. apply CRplus_morph. reflexivity.
   rewrite <- CRplus_assoc. rewrite CRplus_comm, CRopp_plus_distr.
@@ -587,10 +584,10 @@ Lemma CRmin_glb : forall {R : ConstructiveReals} (x y z:CRcarrier R),
 Proof.
   intros. unfold CRmin.
   apply (CRmult_le_reg_r (CR_of_Q R 2)).
-  rewrite <- CR_of_Q_zero. apply CR_of_Q_lt; reflexivity.
+  apply CR_of_Q_lt; reflexivity.
   rewrite CRmult_assoc, <- CR_of_Q_mult.
   setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity.
-  rewrite CR_of_Q_one, CRmult_1_r.
+  rewrite CRmult_1_r.
   apply (CRplus_le_reg_l (CRabs _ (y-x) - (z*CR_of_Q R 2))).
   unfold CRminus. rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r.
   rewrite (CRplus_comm (CRabs R (y + - x) + - (z * CR_of_Q R 2))).
@@ -601,13 +598,13 @@ Proof.
     rewrite CRopp_involutive, (CRplus_comm y), CRplus_assoc.
     apply CRplus_le_compat_l, (CRplus_le_reg_l y).
     rewrite <- CRplus_assoc, CRplus_opp_r, CRplus_0_l.
-    rewrite (CR_of_Q_plus R 1 1), CR_of_Q_one, CRmult_plus_distr_l.
+    rewrite (CR_of_Q_plus R 1 1), CRmult_plus_distr_l.
     rewrite CRmult_1_r. apply CRplus_le_compat; exact H0.
   - rewrite (CRplus_comm x), CRplus_assoc. apply CRplus_le_compat_l.
     apply (CRplus_le_reg_l (-x)).
     rewrite <- CRplus_assoc, CRplus_opp_l, CRplus_0_l.
     rewrite CRopp_mult_distr_l.
-    rewrite (CR_of_Q_plus R 1 1), CR_of_Q_one, CRmult_plus_distr_l.
+    rewrite (CR_of_Q_plus R 1 1), CRmult_plus_distr_l.
     rewrite CRmult_1_r.
     apply CRplus_le_compat; apply CRopp_ge_le_contravar; exact H.
 Qed.
@@ -673,11 +670,11 @@ Lemma CRmax_lub : forall {R : ConstructiveReals} (x y z:CRcarrier R),
     x <= z -> y <= z -> CRmax x y <= z.
 Proof.
   intros. unfold CRmax.
-  apply (CRmult_le_reg_r (CR_of_Q _ 2)). rewrite <- CR_of_Q_zero.
+  apply (CRmult_le_reg_r (CR_of_Q _ 2)).
   apply CR_of_Q_lt; reflexivity.
   rewrite CRmult_assoc, <- CR_of_Q_mult.
   setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity.
-  rewrite CR_of_Q_one, CRmult_1_r.
+  rewrite CRmult_1_r.
   apply (CRplus_le_reg_l (-x-y)).
   rewrite <- CRplus_assoc. unfold CRminus.
   rewrite <- CRopp_plus_distr, CRplus_opp_l, CRplus_0_l.
@@ -687,14 +684,14 @@ Proof.
     rewrite (CRplus_comm x), CRplus_assoc. apply CRplus_le_compat_l.
     apply (CRplus_le_reg_l (-x)).
     rewrite <- CRplus_assoc, CRplus_opp_l, CRplus_0_l.
-    rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CR_of_Q_one, CRmult_1_r.
+    rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CRmult_1_r.
     rewrite CRopp_plus_distr.
     apply CRplus_le_compat; apply CRopp_ge_le_contravar; assumption.
   - rewrite (CRplus_comm y), CRopp_plus_distr, CRplus_assoc.
     apply CRplus_le_compat_l.
     apply (CRplus_le_reg_l y).
     rewrite <- CRplus_assoc, CRplus_opp_r, CRplus_0_l.
-    rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CR_of_Q_one, CRmult_1_r.
+    rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CRmult_1_r.
     apply CRplus_le_compat; assumption.
 Qed.
 
@@ -702,12 +699,12 @@ Lemma CRmax_l : forall {R : ConstructiveReals} (x y : CRcarrier R),
     x <= CRmax x y.
 Proof.
   intros. unfold CRmax.
-  apply (CRmult_le_reg_r (CR_of_Q R 2)). rewrite <- CR_of_Q_zero.
+  apply (CRmult_le_reg_r (CR_of_Q R 2)).
   apply CR_of_Q_lt; reflexivity.
   rewrite CRmult_assoc, <- CR_of_Q_mult.
   setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity.
-  rewrite CR_of_Q_one, CRmult_1_r.
-  setoid_replace 2%Q with (1+1)%Q. rewrite CR_of_Q_plus, CR_of_Q_one.
+  rewrite CRmult_1_r.
+  setoid_replace 2%Q with (1+1)%Q. rewrite CR_of_Q_plus.
   rewrite CRmult_plus_distr_l, CRmult_1_r, CRplus_assoc.
   apply CRplus_le_compat_l.
   apply (CRplus_le_reg_l (-y)).
@@ -720,12 +717,12 @@ Lemma CRmax_r : forall {R : ConstructiveReals} (x y : CRcarrier R),
     y <= CRmax x y.
 Proof.
   intros. unfold CRmax.
-  apply (CRmult_le_reg_r (CR_of_Q _ 2)). rewrite <- CR_of_Q_zero.
+  apply (CRmult_le_reg_r (CR_of_Q _ 2)).
   apply CR_of_Q_lt; reflexivity.
   rewrite CRmult_assoc, <- CR_of_Q_mult.
   setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity.
-  rewrite CR_of_Q_one, CRmult_1_r.
-  rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CR_of_Q_one, CRmult_1_r.
+  rewrite CRmult_1_r.
+  rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CRmult_1_r.
   rewrite (CRplus_comm x).
   rewrite CRplus_assoc. apply CRplus_le_compat_l.
   apply (CRplus_le_reg_l (-x)).
@@ -754,14 +751,14 @@ Proof.
   intros. unfold CRmax.
   setoid_replace (x + z - (x + y)) with (z-y).
   apply (CRmult_eq_reg_r (CR_of_Q _ 2)).
-  left. rewrite <- CR_of_Q_zero. apply CR_of_Q_lt; reflexivity.
+  left. apply CR_of_Q_lt; reflexivity.
   rewrite CRmult_plus_distr_r.
   rewrite CRmult_assoc, <- CR_of_Q_mult.
   setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity.
-  rewrite CR_of_Q_one, CRmult_1_r.
+  rewrite CRmult_1_r.
   rewrite CRmult_assoc, <- CR_of_Q_mult.
   setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity.
-  rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CR_of_Q_one, CRmult_1_r.
+  rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CRmult_1_r.
   rewrite CRmult_1_r.
   do 3 rewrite (CRplus_assoc x). apply CRplus_morph. reflexivity.
   do 2 rewrite <- CRplus_assoc. apply CRplus_morph. 2: reflexivity.
@@ -777,11 +774,11 @@ Lemma CRmax_left : forall {R : ConstructiveReals} (x y : CRcarrier R),
 Proof.
   intros. unfold CRmax.
   apply (CRmult_eq_reg_r (CR_of_Q R 2)).
-  left. rewrite <- CR_of_Q_zero. apply CR_of_Q_lt; reflexivity.
+  left. apply CR_of_Q_lt; reflexivity.
   rewrite CRmult_assoc, <- CR_of_Q_mult.
   setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity.
-  rewrite CR_of_Q_one, CRmult_1_r.
-  rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CR_of_Q_one, CRmult_1_r.
+  rewrite CRmult_1_r.
+  rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CRmult_1_r.
   rewrite CRplus_assoc. apply CRplus_morph. reflexivity.
   rewrite CRabs_left. unfold CRminus. rewrite CRopp_plus_distr, CRopp_involutive.
   rewrite <- CRplus_assoc, CRplus_opp_r, CRplus_0_l. reflexivity.
@@ -793,11 +790,11 @@ Lemma CRmax_right : forall {R : ConstructiveReals} (x y : CRcarrier R),
 Proof.
   intros. unfold CRmax.
   apply (CRmult_eq_reg_r (CR_of_Q R 2)).
-  left. rewrite <- CR_of_Q_zero. apply CR_of_Q_lt; reflexivity.
+  left. apply CR_of_Q_lt; reflexivity.
   rewrite CRmult_assoc, <- CR_of_Q_mult.
   setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity.
-  rewrite CR_of_Q_one, CRmult_1_r.
-  rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CR_of_Q_one, CRmult_1_r.
+  rewrite CRmult_1_r.
+  rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CRmult_1_r.
   rewrite (CRplus_comm x y).
   rewrite CRplus_assoc. apply CRplus_morph. reflexivity.
   rewrite CRabs_right. unfold CRminus. rewrite CRplus_comm.
@@ -812,12 +809,12 @@ Proof.
   rewrite (CRabs_morph
              _ ((x - y + (CRabs _ (a - x) - CRabs _ (a - y))) * CR_of_Q R (1 # 2))).
   rewrite CRabs_mult, (CRabs_right (CR_of_Q R (1 # 2))).
-  2: rewrite <- CR_of_Q_zero; apply CR_of_Q_le; discriminate.
+  2: apply CR_of_Q_le; discriminate.
   apply (CRle_trans
            _ ((CRabs _ (x - y) * 1 + CRabs _ (x-y) * 1)
               * CR_of_Q R (1 # 2))).
   apply CRmult_le_compat_r.
-  rewrite <- CR_of_Q_zero. apply CR_of_Q_le. discriminate.
+  apply CR_of_Q_le. discriminate.
   apply (CRle_trans
            _ (CRabs _ (x - y) + CRabs _ (CRabs _ (a - x) - CRabs _ (a - y)))).
   apply CRabs_triang. rewrite CRmult_1_r. apply CRplus_le_compat_l.
@@ -829,11 +826,11 @@ Proof.
   rewrite CRplus_comm, CRopp_plus_distr, <- CRplus_assoc.
   rewrite CRplus_opp_r, CRopp_involutive, CRplus_0_l.
   reflexivity.
-  rewrite <- CRmult_plus_distr_l, <- CR_of_Q_one.
+  rewrite <- CRmult_plus_distr_l.
   rewrite <- (CR_of_Q_plus R 1 1).
   rewrite CRmult_assoc, <- CR_of_Q_mult.
   setoid_replace ((1 + 1) * (1 # 2))%Q with 1%Q. 2: reflexivity.
-  rewrite CR_of_Q_one, CRmult_1_r. apply CRle_refl.
+  rewrite CRmult_1_r. apply CRle_refl.
   unfold CRminus. rewrite CRopp_mult_distr_l.
   rewrite <- CRmult_plus_distr_r. apply CRmult_morph. 2: reflexivity.
   do 4 rewrite CRplus_assoc. apply CRplus_morph. reflexivity.
@@ -849,10 +846,10 @@ Lemma CRmax_lub_lt : forall {R : ConstructiveReals} (x y z : CRcarrier R),
 Proof.
   intros. unfold CRmax.
   apply (CRmult_lt_reg_r (CR_of_Q R 2)).
-  rewrite <- CR_of_Q_zero. apply CR_of_Q_lt; reflexivity.
+  apply CR_of_Q_lt; reflexivity.
   rewrite CRmult_assoc, <- CR_of_Q_mult.
   setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity.
-  rewrite CR_of_Q_one, CRmult_1_r.
+  rewrite CRmult_1_r.
   apply (CRplus_lt_reg_l _ (-y -x)). unfold CRminus.
   rewrite CRplus_assoc, <- (CRplus_assoc (-x)), <- (CRplus_assoc (-x)).
   rewrite CRplus_opp_l, CRplus_0_l, <- CRplus_assoc, CRplus_opp_l, CRplus_0_l.
@@ -861,14 +858,14 @@ Proof.
     apply CRplus_lt_compat_l.
     apply (CRplus_lt_reg_l _ y).
     rewrite <- CRplus_assoc, CRplus_opp_r, CRplus_0_l.
-    rewrite (CR_of_Q_plus R 1 1), CR_of_Q_one, CRmult_plus_distr_l.
+    rewrite (CR_of_Q_plus R 1 1), CRmult_plus_distr_l.
     rewrite CRmult_1_r. apply CRplus_le_lt_compat.
     apply CRlt_asym, H0. exact H0.
   - rewrite CRopp_plus_distr, CRopp_involutive.
     rewrite CRplus_assoc. apply CRplus_lt_compat_l.
     apply (CRplus_lt_reg_l _ x).
     rewrite <- CRplus_assoc, CRplus_opp_r, CRplus_0_l.
-    rewrite (CR_of_Q_plus R 1 1), CR_of_Q_one, CRmult_plus_distr_l.
+    rewrite (CR_of_Q_plus R 1 1), CRmult_plus_distr_l.
     rewrite CRmult_1_r. apply CRplus_le_lt_compat.
     apply CRlt_asym, H. exact H.
 Qed.
diff --git a/theories/Reals/Abstract/ConstructiveLUB.v b/theories/Reals/Abstract/ConstructiveLUB.v
index 4ae24de154..1c19c6aa40 100644
--- a/theories/Reals/Abstract/ConstructiveLUB.v
+++ b/theories/Reals/Abstract/ConstructiveLUB.v
@@ -108,7 +108,7 @@ Proof.
       rewrite Z.mul_1_l, Z.mul_1_l. apply Pos2Z.pos_le_pos.
       apply Pos2Nat.inj_le. rewrite Nat2Pos.id.
       apply le_S, H0. discriminate.
-      rewrite <- CR_of_Q_zero. apply CR_of_Q_le. discriminate.
+      apply CR_of_Q_le. discriminate.
 Qed.
 
 Lemma is_upper_bound_dec :
@@ -272,7 +272,7 @@ Proof.
       apply CR_of_Q_pos. reflexivity.
       rewrite CRmult_assoc, <- CR_of_Q_mult, (CR_of_Q_plus R 1 1).
       setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity.
-      rewrite CR_of_Q_one, CRmult_plus_distr_l, CRmult_1_r, CRmult_1_r.
+      rewrite CRmult_plus_distr_l, CRmult_1_r, CRmult_1_r.
       apply CRplus_lt_compat_r. exact H0. }
     destruct (CR_cv_open_below _ _ l lcv H1) as [p pmaj].
     assert (0 < (l-CR_of_Q R r) * CR_of_Q R (1#2)).
@@ -280,7 +280,6 @@ Proof.
       apply CRplus_lt_compat_r. exact H0. apply CR_of_Q_pos. reflexivity. }
     destruct (CRup_nat (CRinv R _ (inr H2))) as [i imaj].
     destruct i. exfalso. simpl in imaj.
-    rewrite CR_of_Q_zero in imaj.
     exact (CRlt_asym _ _ imaj (CRinv_0_lt_compat R _ (inr H2) H2)).
     specialize (pmaj (max (S i) (S p)) (le_trans p (S p) _ (le_S p p (le_refl p)) (Nat.le_max_r (S i) (S p)))).
     unfold proj1_sig in pmaj.
@@ -309,7 +308,7 @@ Proof.
          CR_of_Q R (1 # Pos.of_nat (S i)))).
     apply CRlt_asym, imaj. rewrite CRmult_assoc, <- CR_of_Q_mult.
     setoid_replace ((Z.of_nat (S i) # 1) * (1 # Pos.of_nat (S i)))%Q with 1%Q.
-    rewrite CR_of_Q_one, CRmult_1_r.
+    rewrite CRmult_1_r.
     unfold CRminus. rewrite CRmult_plus_distr_r, (CRplus_comm (-CR_of_Q R r)).
     rewrite (CRplus_comm (CR_of_Q R r)), CRmult_plus_distr_r.
     rewrite CRplus_assoc. apply CRplus_le_compat_l.
diff --git a/theories/Reals/Abstract/ConstructiveLimits.v b/theories/Reals/Abstract/ConstructiveLimits.v
index 4a40cc8cb3..64dcd2e1ec 100644
--- a/theories/Reals/Abstract/ConstructiveLimits.v
+++ b/theories/Reals/Abstract/ConstructiveLimits.v
@@ -89,7 +89,7 @@ Lemma CR_cv_unique : forall {R : ConstructiveReals} (xn : nat -> CRcarrier R)
     -> CR_cv R xn b
     -> a == b.
 Proof.
-  intros. assert (CR_cv R (fun _ => CRzero R) (CRminus R b a)).
+  intros. assert (CR_cv R (fun _ => 0) (CRminus R b a)).
   { apply (CR_cv_extens (fun n => CRminus R (xn n) (xn n))).
     intro n. unfold CRminus. apply CRplus_opp_r.
     apply CR_cv_plus. exact H0. apply CR_cv_opp, H. }
@@ -111,8 +111,7 @@ Proof.
     rewrite Qmult_1_r in pmaj. exact pmaj. unfold Qeq, Qnum, Qden; simpl.
     do 2 rewrite Pos.mul_1_r. reflexivity.
     apply (Qplus_lt_l _ _ q). ring_simplify.
-    apply (lt_CR_of_Q R q 0). apply (CRlt_le_trans _ (CRzero R) _ H).
-    apply CR_of_Q_zero.
+    apply (lt_CR_of_Q R q 0). exact H.
     apply (CRlt_le_trans _ (CRopp R z)).
     apply (CRle_lt_trans _ (CRopp R (CR_of_Q R q))). apply CR_of_Q_opp.
     apply CRopp_gt_lt_contravar, H0.
@@ -131,8 +130,7 @@ Proof.
     setoid_replace ((Z.pos p # 1) * (1 # p))%Q with 1%Q in pmaj.
     rewrite Qmult_1_r in pmaj. exact pmaj. unfold Qeq, Qnum, Qden; simpl.
     do 2 rewrite Pos.mul_1_r. reflexivity.
-    apply (lt_CR_of_Q R 0 q). apply (CRle_lt_trans _ (CRzero R)).
-    2: exact H0. apply CR_of_Q_zero.
+    apply (lt_CR_of_Q R 0 q). exact H0.
     apply (CRlt_le_trans _ _ _ H).
     apply (CRle_trans _ (CRabs R (CRopp R z))).
     apply (CRle_trans _ (CRabs R z)).
@@ -140,10 +138,7 @@ Proof.
     apply H1. apply CRle_refl. apply CRabs_opp.
     apply CRabs_morph. unfold CRminus. symmetry. apply CRplus_0_l.
   - subst z. apply (CRplus_eq_reg_l (CRopp R a)).
-    apply (CReq_trans _ (CRzero R)). apply CRplus_opp_l.
-    destruct (CRisRing R).
-    apply (CReq_trans _ (CRplus R b (CRopp R a))). apply CReq_sym, H.
-    apply Radd_comm.
+    rewrite CRplus_opp_l, CRplus_comm. symmetry. exact H.
 Qed.
 
 Lemma CR_cv_eq : forall {R : ConstructiveReals}
@@ -196,7 +191,7 @@ Lemma Un_cv_nat_real : forall {R : ConstructiveReals}
 Proof.
   intros. destruct (CR_archimedean R (CRinv R eps (inr H0))) as [k kmaj].
   assert (0 < CR_of_Q R (Z.pos k # 1)).
-  { rewrite <- CR_of_Q_zero. apply CR_of_Q_lt. reflexivity. }
+  { apply CR_of_Q_lt. reflexivity. }
   specialize (H k) as [p pmaj].
   exists p. intros.
   apply (CRle_lt_trans _ (CR_of_Q R (1 # k))).
@@ -204,7 +199,7 @@ Proof.
   apply (CRmult_lt_reg_l (CR_of_Q R (Z.pos k # 1))). exact H1.
   rewrite <- CR_of_Q_mult.
   apply (CRle_lt_trans _ 1).
-  rewrite <- CR_of_Q_one. apply CR_of_Q_le.
+  apply CR_of_Q_le.
   unfold Qle; simpl. do 2 rewrite Pos.mul_1_r. apply Z.le_refl.
   apply (CRmult_lt_reg_r (CRinv R eps (inr H0))).
   apply CRinv_0_lt_compat, H0. rewrite CRmult_1_l, CRmult_assoc.
@@ -220,7 +215,7 @@ Lemma Un_cv_real_nat : forall {R : ConstructiveReals}
 Proof.
   intros. intros n.
   specialize (H (CR_of_Q R (1#n))) as [p pmaj].
-  rewrite <- CR_of_Q_zero. apply CR_of_Q_lt. reflexivity.
+  apply CR_of_Q_lt. reflexivity.
   exists p. intros. apply CRlt_asym. apply pmaj. apply H.
 Qed.
 
@@ -288,12 +283,12 @@ Proof.
   setoid_replace (1 # n * x)%Q with ((1 # n) *(1# x))%Q. 2: reflexivity.
   rewrite <- (CRmult_1_r (CR_of_Q R (1#n))).
   rewrite CR_of_Q_mult, CRmult_assoc.
-  apply CRmult_le_compat_l. rewrite <- CR_of_Q_zero.
+  apply CRmult_le_compat_l.
   apply CR_of_Q_le. discriminate. intro abs.
   apply (CRmult_lt_compat_l (CR_of_Q R (Z.pos x #1))) in abs.
   rewrite CRmult_1_r, <- CRmult_assoc, <- CR_of_Q_mult in abs.
   rewrite (CR_of_Q_morph R ((Z.pos x # 1) * (1 # x))%Q 1%Q) in abs.
-  rewrite CR_of_Q_one, CRmult_1_l in abs.
+  rewrite CRmult_1_l in abs.
   apply (CRlt_asym _ _ abs), (CRlt_trans _ (1 + CRabs R a)).
   2: exact c. rewrite <- CRplus_0_l, <- CRplus_assoc.
   apply CRplus_lt_compat_r. rewrite CRplus_0_r. apply CRzero_lt_one.
@@ -310,7 +305,7 @@ Lemma CR_cv_const : forall {R : ConstructiveReals} (a : CRcarrier R),
 Proof.
   intros a p. exists O. intros.
   unfold CRminus. rewrite CRplus_opp_r.
-  rewrite CRabs_right. rewrite <- CR_of_Q_zero.
+  rewrite CRabs_right.
   apply CR_of_Q_le. discriminate. apply CRle_refl.
 Qed.
 
@@ -633,7 +628,7 @@ Lemma CR_double : forall {R : ConstructiveReals} (x:CRcarrier R),
     CR_of_Q R 2 * x == x + x.
 Proof.
   intros R x. rewrite (CR_of_Q_morph R 2 (1+1)).
-  2: reflexivity. rewrite CR_of_Q_plus, CR_of_Q_one.
+  2: reflexivity. rewrite CR_of_Q_plus.
   rewrite CRmult_plus_distr_r, CRmult_1_l. reflexivity.
 Qed.
 
@@ -641,7 +636,7 @@ Lemma GeoCvZero : forall {R : ConstructiveReals},
     CR_cv R (fun n:nat => CRpow (CR_of_Q R (1#2)) n) 0.
 Proof.
   intro R. assert (forall n:nat, INR n < CRpow (CR_of_Q R 2) n).
-  { induction n. unfold INR; simpl. rewrite CR_of_Q_zero.
+  { induction n. unfold INR; simpl.
     apply CRzero_lt_one. unfold INR. fold (1+n)%nat.
     rewrite Nat2Z.inj_add.
     rewrite (CR_of_Q_morph R _ ((Z.of_nat 1 # 1) + (Z.of_nat n #1))).
@@ -651,29 +646,29 @@ Proof.
       with (CR_of_Q R 2 * CRpow (CR_of_Q R 2) n).
     2: reflexivity. rewrite CR_double.
     apply CRplus_le_lt_compat.
-    2: exact IHn. simpl. rewrite CR_of_Q_one.
-    apply pow_R1_Rle. rewrite <- CR_of_Q_one. apply CR_of_Q_le. discriminate. }
+    2: exact IHn. simpl.
+    apply pow_R1_Rle. apply CR_of_Q_le. discriminate. }
   intros p. exists (Pos.to_nat p). intros.
   unfold CRminus. rewrite CRopp_0. rewrite CRplus_0_r.
   rewrite CRabs_right.
-  2: apply pow_le; rewrite <- CR_of_Q_zero; apply CR_of_Q_le; discriminate.
+  2: apply pow_le; apply CR_of_Q_le; discriminate.
   apply CRlt_asym.
   apply (CRmult_lt_reg_l (CR_of_Q R (Z.pos p # 1))).
-  rewrite <- CR_of_Q_zero. apply CR_of_Q_lt. reflexivity. rewrite <- CR_of_Q_mult.
+  apply CR_of_Q_lt. reflexivity. rewrite <- CR_of_Q_mult.
   rewrite (CR_of_Q_morph R ((Z.pos p # 1) * (1 # p)) 1).
   2: unfold Qmult, Qeq, Qnum, Qden; ring_simplify; reflexivity.
   apply (CRmult_lt_reg_r (CRpow (CR_of_Q R 2) i)).
-  apply pow_lt. simpl. rewrite <- CR_of_Q_zero.
+  apply pow_lt. simpl.
   apply CR_of_Q_lt. reflexivity.
   rewrite CRmult_assoc. rewrite pow_mult.
   rewrite (pow_proper (CR_of_Q R (1 # 2) * CR_of_Q R 2) 1), pow_one.
-  rewrite CRmult_1_r, CR_of_Q_one, CRmult_1_l.
+  rewrite CRmult_1_r, CRmult_1_l.
   apply (CRle_lt_trans _ (INR i)). 2: exact (H i). clear H.
   apply CR_of_Q_le. unfold Qle,Qnum,Qden.
   do 2 rewrite Z.mul_1_r.
   rewrite <- positive_nat_Z. apply Nat2Z.inj_le, H0.
   rewrite <- CR_of_Q_mult. setoid_replace ((1#2)*2)%Q with 1%Q.
-  apply CR_of_Q_one. reflexivity.
+  reflexivity. reflexivity.
 Qed.
 
 Lemma GeoFiniteSum : forall {R : ConstructiveReals} (n:nat),
@@ -681,9 +676,9 @@ Lemma GeoFiniteSum : forall {R : ConstructiveReals} (n:nat),
 Proof.
   induction n.
   - unfold CRsum, CRpow. simpl (1%ConstructiveReals).
-    unfold CRminus. rewrite (CR_of_Q_morph R _ (1+1)).
-    rewrite CR_of_Q_plus, CR_of_Q_one, CRplus_assoc.
-    rewrite CRplus_opp_r, CRplus_0_r. reflexivity. reflexivity.
+    unfold CRminus. rewrite (CR_of_Q_plus R 1 1).
+    rewrite CRplus_assoc.
+    rewrite CRplus_opp_r, CRplus_0_r. reflexivity.
   - setoid_replace (CRsum (CRpow (CR_of_Q R (1 # 2))) (S n))
       with (CRsum (CRpow (CR_of_Q R (1 # 2))) n + CRpow (CR_of_Q R (1 # 2)) (S n)).
     2: reflexivity.
@@ -701,7 +696,7 @@ Proof.
     2: reflexivity.
     rewrite <- CRmult_assoc, <- CR_of_Q_mult.
     setoid_replace (2 * (1 # 2))%Q with 1%Q.
-    rewrite CR_of_Q_one. apply CRmult_1_l. reflexivity.
+    apply CRmult_1_l. reflexivity.
 Qed.
 
 Lemma GeoHalfBelowTwo : forall {R : ConstructiveReals} (n:nat),
@@ -710,7 +705,7 @@ Proof.
   intros. rewrite <- (CRplus_0_r (CR_of_Q R 2)), GeoFiniteSum.
   apply CRplus_lt_compat_l. rewrite <- CRopp_0.
   apply CRopp_gt_lt_contravar.
-  apply pow_lt. rewrite <- CR_of_Q_zero. apply CR_of_Q_lt. reflexivity.
+  apply pow_lt. apply CR_of_Q_lt. reflexivity.
 Qed.
 
 Lemma GeoHalfTwo : forall {R : ConstructiveReals},
@@ -720,35 +715,35 @@ Proof.
   apply (CR_cv_eq _ (fun n => CR_of_Q R 2 - CRpow (CR_of_Q R (1 # 2)) n)).
   - intro n. rewrite GeoFiniteSum. reflexivity.
   - assert (forall n:nat, INR n < CRpow (CR_of_Q R 2) n).
-    { induction n. unfold INR; simpl. rewrite CR_of_Q_zero.
+    { induction n. unfold INR; simpl.
       apply CRzero_lt_one. apply (CRlt_le_trans _ (CRpow (CR_of_Q R 2) n + 1)).
       unfold INR.
       rewrite Nat2Z.inj_succ, <- Z.add_1_l.
       rewrite (CR_of_Q_morph R _ (1 + (Z.of_nat n #1))).
       2: symmetry; apply Qinv_plus_distr. rewrite CR_of_Q_plus.
-      rewrite CRplus_comm. rewrite CR_of_Q_one.
+      rewrite CRplus_comm.
       apply CRplus_lt_compat_r, IHn.
       setoid_replace (CRpow (CR_of_Q R 2) (S n))
         with (CRpow (CR_of_Q R 2) n + CRpow (CR_of_Q R 2) n).
       apply CRplus_le_compat. apply CRle_refl.
-      apply pow_R1_Rle. rewrite <- CR_of_Q_one. apply CR_of_Q_le. discriminate.
+      apply pow_R1_Rle. apply CR_of_Q_le. discriminate.
       rewrite <- CR_double. reflexivity. }
     intros n. exists (Pos.to_nat n). intros.
     setoid_replace (CR_of_Q R 2 - CRpow (CR_of_Q R (1 # 2)) i - CR_of_Q R 2)
       with (- CRpow (CR_of_Q R (1 # 2)) i).
     rewrite CRabs_opp. rewrite CRabs_right.
     assert (0 < CR_of_Q R 2).
-    { rewrite <- CR_of_Q_zero. apply CR_of_Q_lt. reflexivity. }
+    { apply CR_of_Q_lt. reflexivity. }
     rewrite (pow_proper _ (CRinv R (CR_of_Q R 2) (inr H1))).
     rewrite pow_inv. apply CRlt_asym.
     apply (CRmult_lt_reg_l (CRpow (CR_of_Q R 2) i)). apply pow_lt, H1.
     rewrite CRinv_r.
     apply (CRmult_lt_reg_r (CR_of_Q R (Z.pos n#1))).
-    rewrite <- CR_of_Q_zero. apply CR_of_Q_lt. reflexivity.
+    apply CR_of_Q_lt. reflexivity.
     rewrite CRmult_1_l, CRmult_assoc.
     rewrite <- CR_of_Q_mult.
     rewrite (CR_of_Q_morph R ((1 # n) * (Z.pos n # 1)) 1). 2: reflexivity.
-    rewrite CR_of_Q_one, CRmult_1_r. apply (CRle_lt_trans _ (INR i)).
+    rewrite CRmult_1_r. apply (CRle_lt_trans _ (INR i)).
     2: apply H. apply CR_of_Q_le.
     unfold Qle, Qnum, Qden. do 2 rewrite Z.mul_1_r. destruct i.
     exfalso. inversion H0. pose proof (Pos2Nat.is_pos n).
@@ -758,8 +753,8 @@ Proof.
     apply (CRmult_eq_reg_l (CR_of_Q R 2)). right. exact H1.
     rewrite CRinv_r. rewrite <- CR_of_Q_mult.
     setoid_replace (2 * (1 # 2))%Q with 1%Q.
-    apply CR_of_Q_one. reflexivity.
-    apply CRlt_asym, pow_lt. rewrite <- CR_of_Q_zero.
+    reflexivity. reflexivity.
+    apply CRlt_asym, pow_lt.
     apply CR_of_Q_lt. reflexivity.
     unfold CRminus. rewrite CRplus_comm, <- CRplus_assoc.
     rewrite CRplus_opp_l, CRplus_0_l. reflexivity.
@@ -929,5 +924,5 @@ Proof.
     intros n. exists (Pos.to_nat n). intros.
     unfold CRminus. simpl.
     rewrite CRopp_involutive, CRplus_opp_l. rewrite CRabs_right.
-    rewrite <- CR_of_Q_zero. apply CR_of_Q_le. discriminate. apply CRle_refl.
+    apply CR_of_Q_le. discriminate. apply CRle_refl.
 Qed.
diff --git a/theories/Reals/Abstract/ConstructiveReals.v b/theories/Reals/Abstract/ConstructiveReals.v
index d91fd1183a..019428a5b0 100644
--- a/theories/Reals/Abstract/ConstructiveReals.v
+++ b/theories/Reals/Abstract/ConstructiveReals.v
@@ -101,9 +101,15 @@ Structure ConstructiveReals : Type :=
     CRltDisjunctEpsilon : forall a b c d : CRcarrier,
         (CRltProp a b \/ CRltProp c d) -> CRlt a b  +  CRlt c d;
 
-    (* Constants *)
-    CRzero : CRcarrier;
-    CRone : CRcarrier;
+    (* The initial field morphism (in characteristic zero).
+       The abstract definition by iteration of addition is
+       probably the slowest. Let each instance implement
+       a faster (and often simpler) version. *)
+    CR_of_Q : Q -> CRcarrier;
+    CR_of_Q_lt : forall q r : Q,
+        Qlt q r -> CRlt (CR_of_Q q) (CR_of_Q r);
+    lt_CR_of_Q : forall q r : Q,
+        CRlt (CR_of_Q q) (CR_of_Q r) -> Qlt q r;
 
     (* Addition and multiplication *)
     CRplus : CRcarrier -> CRcarrier -> CRcarrier;
@@ -111,19 +117,22 @@ Structure ConstructiveReals : Type :=
                          stronger than Prop-existence of opposite *)
     CRmult : CRcarrier -> CRcarrier -> CRcarrier;
 
-    CRisRing : ring_theory CRzero CRone CRplus CRmult
+    CR_of_Q_plus : forall q r : Q, CReq (CR_of_Q (q+r))
+                                           (CRplus (CR_of_Q q) (CR_of_Q r));
+    CR_of_Q_mult : forall q r : Q, CReq (CR_of_Q (q*r))
+                                           (CRmult (CR_of_Q q) (CR_of_Q r));
+    CRisRing : ring_theory (CR_of_Q 0) (CR_of_Q 1) CRplus CRmult
                           (fun x y => CRplus x (CRopp y)) CRopp CReq;
     CRisRingExt : ring_eq_ext CRplus CRmult CRopp CReq;
 
     (* 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. *)
+    CRzero_lt_one : CRlt (CR_of_Q 0) (CR_of_Q 1);
     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);
+        CRlt (CR_of_Q 0) x -> CRlt (CR_of_Q 0) y -> CRlt (CR_of_Q 0) (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.
@@ -132,26 +141,11 @@ Structure ConstructiveReals : Type :=
 
        To implement Finv by Cauchy sequences we need orderAppart,
        ~orderEq is not enough. *)
-    CRinv : forall x : CRcarrier, CRapart x CRzero -> CRcarrier;
-    CRinv_l : forall (r:CRcarrier) (rnz : CRapart r CRzero),
-        CReq (CRmult (CRinv r rnz) r) CRone;
-    CRinv_0_lt_compat : forall (r : CRcarrier) (rnz : CRapart r CRzero),
-        CRlt CRzero r -> CRlt CRzero (CRinv r rnz);
-
-    (* The initial field morphism (in characteristic zero).
-       The abstract definition by iteration of addition is
-       probably the slowest. Let each instance implement
-       a faster (and often simpler) version. *)
-    CR_of_Q : Q -> CRcarrier;
-    CR_of_Q_plus : forall q r : Q, CReq (CR_of_Q (q+r))
-                                           (CRplus (CR_of_Q q) (CR_of_Q r));
-    CR_of_Q_mult : forall q r : Q, CReq (CR_of_Q (q*r))
-                                           (CRmult (CR_of_Q q) (CR_of_Q r));
-    CR_of_Q_one : CReq (CR_of_Q 1) CRone;
-    CR_of_Q_lt : forall q r : Q,
-        Qlt q r -> CRlt (CR_of_Q q) (CR_of_Q r);
-    lt_CR_of_Q : forall q r : Q,
-        CRlt (CR_of_Q q) (CR_of_Q r) -> Qlt q r;
+    CRinv : forall x : CRcarrier, CRapart x (CR_of_Q 0) -> CRcarrier;
+    CRinv_l : forall (r:CRcarrier) (rnz : CRapart r (CR_of_Q 0)),
+        CReq (CRmult (CRinv r rnz) r) (CR_of_Q 1);
+    CRinv_0_lt_compat : forall (r : CRcarrier) (rnz : CRapart r (CR_of_Q 0)),
+        CRlt (CR_of_Q 0) r -> CRlt (CR_of_Q 0) (CRinv r rnz);
 
     (* This function is very fast in both the Cauchy and Dedekind
        instances, because this rational number q is almost what
@@ -213,8 +207,17 @@ Notation "x <= y <= z" := (CRle _ x y /\ CRle _ y z) : ConstructiveReals.
 Notation "x < y < z"   := (prod (CRlt _ x y) (CRlt _ y z)) : ConstructiveReals.
 Notation "x == y" := (CReq _ x y) : ConstructiveReals.
 Notation "x ≶ y" := (CRapart _ x y) (at level 70, no associativity) : ConstructiveReals.
-Notation "0" := (CRzero _) : ConstructiveReals.
-Notation "1" := (CRone _) : ConstructiveReals.
+Notation "0" := (CR_of_Q _ 0) : ConstructiveReals.
+Notation "1" := (CR_of_Q _ 1) : ConstructiveReals.
+Notation "2" := (CR_of_Q _ 2) : ConstructiveReals.
+Notation "3" := (CR_of_Q _ 3) : ConstructiveReals.
+Notation "4" := (CR_of_Q _ 4) : ConstructiveReals.
+Notation "5" := (CR_of_Q _ 5) : ConstructiveReals.
+Notation "6" := (CR_of_Q _ 6) : ConstructiveReals.
+Notation "7" := (CR_of_Q _ 7) : ConstructiveReals.
+Notation "8" := (CR_of_Q _ 8) : ConstructiveReals.
+Notation "9" := (CR_of_Q _ 9) : ConstructiveReals.
+Notation "10" := (CR_of_Q _ 10) : ConstructiveReals.
 Notation "x + y" := (CRplus _ x y) : ConstructiveReals.
 Notation "- x" := (CRopp _ x) : ConstructiveReals.
 Notation "x - y" := (CRminus _ x y) : ConstructiveReals.
@@ -567,7 +570,7 @@ Lemma CRopp_involutive : forall {R : ConstructiveReals} (r : CRcarrier R),
     - - r == r.
 Proof.
   intros. apply (CRplus_eq_reg_l (CRopp R r)).
-  transitivity (CRzero R). apply CRisRing.
+  transitivity (CR_of_Q R 0). apply CRisRing.
   apply CReq_sym. transitivity (r + - r).
   apply CRisRing. apply CRisRing.
 Qed.
@@ -578,7 +581,7 @@ Lemma CRopp_gt_lt_contravar
 Proof.
   intros. apply (CRplus_lt_reg_l R r1).
   destruct (CRisRing R).
-  apply (CRle_lt_trans _ (CRzero R)). apply Ropp_def.
+  apply (CRle_lt_trans _ 0). apply Ropp_def.
   apply (CRplus_lt_compat_l R (CRopp R r2)) in H.
   apply (CRle_lt_trans _ (CRplus R (CRopp R r2) r2)).
   apply (CRle_trans _ (CRplus R r2 (CRopp R r2))).
@@ -611,13 +614,13 @@ Lemma CRopp_plus_distr : forall {R : ConstructiveReals} (r1 r2 : CRcarrier R),
 Proof.
   intros. destruct (CRisRing R), (CRisRingExt R).
   apply (CRplus_eq_reg_l (CRplus R r1 r2)).
-  transitivity (CRzero R). apply Ropp_def.
+  transitivity (CR_of_Q R 0). apply Ropp_def.
   transitivity (r2 + r1 + (-r1 + -r2)).
   transitivity (r2 + (r1 + (-r1 + -r2))).
   transitivity (r2 + - r2).
   apply CReq_sym. apply Ropp_def. apply Radd_ext.
   apply CReq_refl.
-  transitivity (CRzero R + - r2).
+  transitivity (0 + - r2).
   apply CReq_sym, Radd_0_l.
   transitivity (r1 + - r1 + - r2).
   apply Radd_ext. 2: apply CReq_refl. apply CReq_sym, Ropp_def.
@@ -701,7 +704,7 @@ Lemma CRopp_mult_distr_r : forall {R : ConstructiveReals} (r1 r2 : CRcarrier R),
     - (r1 * r2) == r1 * (- r2).
 Proof.
   intros. apply (CRplus_eq_reg_l (CRmult R r1 r2)).
-  destruct (CRisRing R). transitivity (CRzero R). apply Ropp_def.
+  destruct (CRisRing R). transitivity (CR_of_Q R 0). apply Ropp_def.
   transitivity (r1 * (r2 + - r2)).
   2: apply CRmult_plus_distr_l.
   transitivity (r1 * 0).
@@ -725,7 +728,7 @@ Lemma CRmult_lt_compat_r : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R
     0 < r -> r1 < r2 -> r1 * r < r2 * r.
 Proof.
   intros. apply (CRplus_lt_reg_r (CRopp R (CRmult R r1 r))).
-  apply (CRle_lt_trans _ (CRzero R)).
+  apply (CRle_lt_trans _ 0).
   apply (Ropp_def (CRisRing R)).
   apply (CRlt_le_trans _ (CRplus R (CRmult R r2 r) (CRmult R (CRopp R r1) r))).
   apply (CRlt_le_trans _ (CRmult R (CRplus R r2 (CRopp R r1)) r)).
@@ -734,7 +737,7 @@ Proof.
   apply (CRle_lt_trans _ r1). apply (Radd_0_l (CRisRing R)).
   apply (CRlt_le_trans _ r2 _ H0).
   apply (CRle_trans _ (CRplus R r2 (CRplus R (CRopp R r1) r1))).
-  apply (CRle_trans _ (CRplus R r2 (CRzero R))).
+  apply (CRle_trans _ (CRplus R r2 0)).
   destruct (CRplus_0_r r2). exact H1.
   apply CRplus_le_compat_l. destruct (CRplus_opp_l r1). exact H1.
   destruct (Radd_assoc (CRisRing R) r2 (CRopp R r1) r1). exact H2.
@@ -752,7 +755,7 @@ Proof.
 Qed.
 
 Lemma CRinv_r : forall {R : ConstructiveReals} (r:CRcarrier R)
-                  (rnz : r ≶ (CRzero R)),
+                  (rnz : r ≶ 0),
     r * (/ r) rnz == 1.
 Proof.
   intros. transitivity ((/ r) rnz * r).
@@ -765,7 +768,7 @@ Proof.
   intros. apply (CRmult_lt_compat_r ((/ r) (inr H))) in H0.
   2: apply CRinv_0_lt_compat, H.
   apply (CRle_lt_trans _ ((r1 * r) * ((/ r) (inr H)))).
-  - clear H0. apply (CRle_trans _ (CRmult R r1 (CRone R))).
+  - clear H0. apply (CRle_trans _ (CRmult R r1 1)).
     destruct (CRmult_1_r r1). exact H0.
     apply (CRle_trans _ (CRmult R r1 (CRmult R r ((/ r) (inr H))))).
     destruct (Rmul_ext (CRisRingExt R) r1 r1 (CReq_refl r1)
@@ -779,7 +782,7 @@ Proof.
     apply (CRle_trans _ (r2 * (r * ((/ r) (inr H))))).
     destruct (Rmul_assoc (CRisRing R) r2 r ((/ r) (inr H))). exact H0.
     destruct (Rmul_ext (CRisRingExt R) r2 r2 (CReq_refl r2)
-                       (r * ((/ r) (inr H))) (CRone R)).
+                       (r * ((/ r) (inr H))) 1).
     apply CRinv_r. exact H1.
 Qed.
 
@@ -829,7 +832,7 @@ Proof.
       apply CRmult_lt_compat_r. 2: exact abs.
       apply (CRplus_lt_reg_r r). apply (CRle_lt_trans _ r).
       apply (Radd_0_l (CRisRing R)).
-      apply (CRlt_le_trans _ (CRzero R) _ c).
+      apply (CRlt_le_trans _ 0 _ c).
       apply CRplus_opp_l.
     + intro abs. apply H0. apply CRopp_lt_cancel.
       apply (CRle_lt_trans _ (CRmult R r2 (CRopp R r))).
@@ -839,7 +842,7 @@ Proof.
       apply CRmult_lt_compat_r. 2: exact abs.
       apply (CRplus_lt_reg_r r). apply (CRle_lt_trans _ r).
       apply (Radd_0_l (CRisRing R)).
-      apply (CRlt_le_trans _ (CRzero R) _ c).
+      apply (CRlt_le_trans _ 0 _ c).
       apply CRplus_opp_l.
 Qed.
 
@@ -920,31 +923,21 @@ Proof.
   intros R x y H. apply CR_of_Q_morph; assumption.
 Qed.
 
-Lemma CR_of_Q_zero : forall {R : ConstructiveReals},
-    CR_of_Q R 0 == 0.
-Proof.
-  intros. apply CRzero_double.
-  transitivity (CR_of_Q R (0+0)). apply CR_of_Q_morph.
-  reflexivity. apply CR_of_Q_plus.
-Qed.
-
 Lemma CR_of_Q_opp : forall {R : ConstructiveReals} (q : Q),
     CR_of_Q R (-q) == - CR_of_Q R q.
 Proof.
   intros. apply (CRplus_eq_reg_l (CR_of_Q R q)).
-  transitivity (CRzero R).
+  transitivity (CR_of_Q R 0).
   transitivity (CR_of_Q R (q-q)).
   apply CReq_sym, CR_of_Q_plus.
-  transitivity (CR_of_Q R 0).
-  apply CR_of_Q_morph. ring. apply CR_of_Q_zero.
+  apply CR_of_Q_morph. ring.
   apply CReq_sym. apply (CRisRing R).
 Qed.
 
 Lemma CR_of_Q_pos : forall {R : ConstructiveReals} (q:Q),
     Qlt 0 q -> 0 < CR_of_Q R q.
 Proof.
-  intros. apply (CRle_lt_trans _ (CR_of_Q R 0)).
-  apply CR_of_Q_zero. apply CR_of_Q_lt. exact H.
+  intros. apply CR_of_Q_lt. exact H.
 Qed.
 
 Lemma CR_of_Q_inv : forall {R : ConstructiveReals} (q : Q) (qPos : Qlt 0 q),
@@ -954,7 +947,7 @@ Proof.
   intros.
   apply (CRmult_eq_reg_l (CR_of_Q R q)).
   right. apply CR_of_Q_pos, qPos.
-  rewrite CRinv_r, <- CR_of_Q_mult, <- CR_of_Q_one.
+  rewrite CRinv_r, <- CR_of_Q_mult.
   apply CR_of_Q_morph. field. intro abs.
   rewrite abs in qPos. exact (Qlt_irrefl 0 qPos).
 Qed.
@@ -969,7 +962,7 @@ Proof.
   destruct (CR_archimedean R (b * ((/ -(a*b)) (inr epsPos))))
     as [n maj].
   assert (0 < CR_of_Q R (Z.pos n #1)) as nPos.
-  { rewrite <- CR_of_Q_zero. apply CR_of_Q_lt. reflexivity. }
+  { apply CR_of_Q_lt. reflexivity. }
   assert (b * (/ CR_of_Q R (Z.pos n #1)) (inr nPos) < -(a*b)).
   { apply (CRmult_lt_reg_r (CR_of_Q R (Z.pos n #1))). apply nPos.
     rewrite <- (Rmul_assoc (CRisRing R)), CRinv_l, CRmult_1_r.
@@ -1082,7 +1075,7 @@ Definition CRfloor {R : ConstructiveReals} (a : CRcarrier R)
 Proof.
   destruct (CR_Q_dense R (a - CR_of_Q R (1#2)) a) as [q qmaj].
   - apply (CRlt_le_trans _ (a-0)). apply CRplus_lt_compat_l.
-    apply CRopp_gt_lt_contravar. rewrite <- CR_of_Q_zero.
+    apply CRopp_gt_lt_contravar.
     apply CR_of_Q_lt. reflexivity.
     unfold CRminus. rewrite CRopp_0, CRplus_0_r. apply CRle_refl.
   - exists (Qfloor q). destruct qmaj. split.
diff --git a/theories/Reals/Abstract/ConstructiveRealsMorphisms.v b/theories/Reals/Abstract/ConstructiveRealsMorphisms.v
index bc44668e2f..cf302dc847 100644
--- a/theories/Reals/Abstract/ConstructiveRealsMorphisms.v
+++ b/theories/Reals/Abstract/ConstructiveRealsMorphisms.v
@@ -163,9 +163,8 @@ Lemma CRmorph_zero : forall {R1 R2 : ConstructiveReals}
     CRmorph f 0 == 0.
 Proof.
   intros. apply (CReq_trans _ (CRmorph f (CR_of_Q R1 0))).
-  apply CRmorph_proper. apply CReq_sym, CR_of_Q_zero.
-  apply (CReq_trans _ (CR_of_Q R2 0)).
-  apply CRmorph_rat. apply CR_of_Q_zero.
+  apply CRmorph_proper. reflexivity.
+  apply CRmorph_rat.
 Qed.
 
 Lemma CRmorph_one : forall {R1 R2 : ConstructiveReals}
@@ -173,9 +172,8 @@ Lemma CRmorph_one : forall {R1 R2 : ConstructiveReals}
     CRmorph f 1 == 1.
 Proof.
   intros. apply (CReq_trans _ (CRmorph f (CR_of_Q R1 1))).
-  apply CRmorph_proper. apply CReq_sym, CR_of_Q_one.
-  apply (CReq_trans _ (CR_of_Q R2 1)).
-  apply CRmorph_rat. apply CR_of_Q_one.
+  apply CRmorph_proper. reflexivity.
+  apply CRmorph_rat.
 Qed.
 
 Lemma CRmorph_opp : forall {R1 R2 : ConstructiveReals}
@@ -228,9 +226,9 @@ Lemma CRplus_pos_rat_lt : forall {R : ConstructiveReals} (x : CRcarrier R) (q :
     Qlt 0 q -> CRlt R x (CRplus R x (CR_of_Q R q)).
 Proof.
   intros.
-  apply (CRle_lt_trans _ (CRplus R x (CRzero R))). apply CRplus_0_r.
+  apply (CRle_lt_trans _ (CRplus R x 0)). apply CRplus_0_r.
   apply CRplus_lt_compat_l.
-  apply (CRle_lt_trans _ (CR_of_Q R 0)). apply CR_of_Q_zero.
+  apply (CRle_lt_trans _ (CR_of_Q R 0)). apply CRle_refl.
   apply CR_of_Q_lt. exact H.
 Defined.
 
@@ -238,10 +236,10 @@ Lemma CRplus_neg_rat_lt : forall {R : ConstructiveReals} (x : CRcarrier R) (q :
     Qlt q 0 -> CRlt R (CRplus R x (CR_of_Q R q)) x.
 Proof.
   intros.
-  apply (CRlt_le_trans _ (CRplus R x (CRzero R))). 2: apply CRplus_0_r.
+  apply (CRlt_le_trans _ (CRplus R x 0)). 2: apply CRplus_0_r.
   apply CRplus_lt_compat_l.
   apply (CRlt_le_trans _ (CR_of_Q R 0)).
-  apply CR_of_Q_lt. exact H. apply CR_of_Q_zero.
+  apply CR_of_Q_lt. exact H. apply CRle_refl.
 Qed.
 
 Lemma CRmorph_plus_rat : forall {R1 R2 : ConstructiveReals}
@@ -276,7 +274,7 @@ Proof.
     destruct (CRisRing R1).
     apply (CRle_trans
              _ (CRplus R1 x (CRplus R1 (CR_of_Q R1 q) (CRopp R1 (CR_of_Q R1 q))))).
-    apply (CRle_trans _ (CRplus R1 x (CRzero R1))).
+    apply (CRle_trans _ (CRplus R1 x 0)).
     destruct (CRplus_0_r x). exact H.
     apply CRplus_le_compat_l. destruct (Ropp_def (CR_of_Q R1 q)). exact H.
     destruct (Radd_assoc x (CR_of_Q R1 q) (CRopp R1 (CR_of_Q R1 q))).
@@ -294,7 +292,7 @@ Proof.
              _ (CRplus R1 x (CRplus R1 (CR_of_Q R1 q) (CRopp R1 (CR_of_Q R1 q))))).
     destruct (Radd_assoc x (CR_of_Q R1 q) (CRopp R1 (CR_of_Q R1 q))).
     exact H0.
-    apply (CRle_trans _ (CRplus R1 x (CRzero R1))).
+    apply (CRle_trans _ (CRplus R1 x 0)).
     apply CRplus_le_compat_l. destruct (Ropp_def (CR_of_Q R1 q)). exact H1.
     destruct (CRplus_0_r x). exact H1.
     apply (CRlt_le_trans _ (CR_of_Q R1 (r-q))).
@@ -379,12 +377,12 @@ Proof.
     apply CRmorph_proper. destruct (CRisRing R1).
     apply (CReq_trans _ (CRplus R1 x (CRplus R1 y (CRopp R1 y)))).
     apply CReq_sym, Radd_assoc.
-    apply (CReq_trans _ (CRplus R1 x (CRzero R1))). 2: apply CRplus_0_r.
+    apply (CReq_trans _ (CRplus R1 x 0)). 2: apply CRplus_0_r.
     destruct (CRisRingExt R1). apply Radd_ext.
     apply CReq_refl. apply Ropp_def.
     apply (CRplus_lt_reg_r (CRmorph f y)).
     apply (CRlt_le_trans _ _ _ abs). clear abs.
-    apply (CRle_trans _ (CRplus R2 (CRmorph f (CRplus R1 x y)) (CRzero R2))).
+    apply (CRle_trans _ (CRplus R2 (CRmorph f (CRplus R1 x y)) 0)).
     destruct (CRplus_0_r (CRmorph f (CRplus R1 x y))). exact H.
     apply (CRle_trans _ (CRplus R2 (CRmorph f (CRplus R1 x y))
                                 (CRplus R2 (CRmorph f (CRopp R1 y)) (CRmorph f y)))).
@@ -407,29 +405,26 @@ Lemma CRmorph_mult_pos : forall {R1 R2 : ConstructiveReals}
 Proof.
   induction n.
   - simpl. destruct (CRisRingExt R1).
-    apply (CReq_trans _ (CRzero R2)).
-    + apply (CReq_trans _ (CRmorph f (CRzero R1))).
+    apply (CReq_trans _ 0).
+    + apply (CReq_trans _ (CRmorph f 0)).
       2: apply CRmorph_zero. apply CRmorph_proper.
-      apply (CReq_trans _ (CRmult R1 x (CRzero R1))).
-      2: apply CRmult_0_r. apply Rmul_ext. apply CReq_refl. apply CR_of_Q_zero.
-    + apply (CReq_trans _ (CRmult R2 (CRmorph f x) (CRzero R2))).
+      apply (CReq_trans _ (CRmult R1 x 0)).
+      2: apply CRmult_0_r. apply Rmul_ext. apply CReq_refl. reflexivity.
+    + apply (CReq_trans _ (CRmult R2 (CRmorph f x) 0)).
       apply CReq_sym, CRmult_0_r. destruct (CRisRingExt R2).
-      apply Rmul_ext0. apply CReq_refl. apply CReq_sym, CR_of_Q_zero.
+      apply Rmul_ext0. apply CReq_refl. reflexivity.
   - destruct (CRisRingExt R1), (CRisRingExt R2).
-    apply (CReq_trans
-             _  (CRmorph f (CRplus R1 x (CRmult R1 x (CR_of_Q R1 (Z.of_nat n # 1)))))).
+    transitivity (CRmorph f (CRplus R1 x (CRmult R1 x (CR_of_Q R1 (Z.of_nat n # 1))))).
     apply CRmorph_proper.
-    apply (CReq_trans
-             _ (CRmult R1 x (CRplus R1 (CRone R1) (CR_of_Q R1 (Z.of_nat n # 1))))).
-    apply Rmul_ext. apply CReq_refl.
-    apply (CReq_trans _ (CR_of_Q R1 (1 + (Z.of_nat n # 1)))).
+    transitivity (CRmult R1 x (CRplus R1 1 (CR_of_Q R1 (Z.of_nat n # 1)))).
+    apply Rmul_ext. reflexivity.
+    transitivity (CR_of_Q R1 (1 + (Z.of_nat n # 1))).
     apply CR_of_Q_morph. rewrite Nat2Z.inj_succ. unfold Z.succ.
     rewrite Z.add_comm. rewrite Qinv_plus_distr. reflexivity.
-    apply (CReq_trans _ (CRplus R1 (CR_of_Q R1 1) (CR_of_Q R1 (Z.of_nat n # 1)))).
-    apply CR_of_Q_plus. apply Radd_ext. apply CR_of_Q_one. apply CReq_refl.
-    apply (CReq_trans _ (CRplus R1 (CRmult R1 x (CRone R1))
-                                (CRmult R1 x (CR_of_Q R1 (Z.of_nat n # 1))))).
-    apply CRmult_plus_distr_l. apply Radd_ext. apply CRmult_1_r. apply CReq_refl.
+    rewrite CR_of_Q_plus. reflexivity.
+    transitivity (CRplus R1 (CRmult R1 x 1)
+                         (CRmult R1 x (CR_of_Q R1 (Z.of_nat n # 1)))).
+    apply CRmult_plus_distr_l. apply Radd_ext. apply CRmult_1_r. reflexivity.
     apply (CReq_trans
              _ (CRplus R2 (CRmorph f x)
                        (CRmorph f (CRmult R1 x (CR_of_Q R1 (Z.of_nat n # 1)))))).
@@ -439,16 +434,16 @@ Proof.
                        (CRmult R2 (CRmorph f x) (CR_of_Q R2 (Z.of_nat n # 1))))).
     apply Radd_ext0. apply CReq_refl. exact IHn.
     apply (CReq_trans
-             _ (CRmult R2 (CRmorph f x) (CRplus R2 (CRone R2) (CR_of_Q R2 (Z.of_nat n # 1))))).
+             _ (CRmult R2 (CRmorph f x) (CRplus R2 1 (CR_of_Q R2 (Z.of_nat n # 1))))).
     apply (CReq_trans
-             _ (CRplus R2 (CRmult R2 (CRmorph f x) (CRone R2))
+             _ (CRplus R2 (CRmult R2 (CRmorph f x) 1)
                        (CRmult R2 (CRmorph f x) (CR_of_Q R2 (Z.of_nat n # 1))))).
     apply Radd_ext0. 2: apply CReq_refl. apply CReq_sym, CRmult_1_r.
     apply CReq_sym, CRmult_plus_distr_l.
     apply Rmul_ext0. apply CReq_refl.
     apply (CReq_trans _ (CR_of_Q R2 (1 + (Z.of_nat n # 1)))).
     apply (CReq_trans _ (CRplus R2 (CR_of_Q R2 1) (CR_of_Q R2 (Z.of_nat n # 1)))).
-    apply Radd_ext0. apply CReq_sym, CR_of_Q_one. apply CReq_refl.
+    apply Radd_ext0. reflexivity. reflexivity.
     apply CReq_sym, CR_of_Q_plus.
     apply CR_of_Q_morph. rewrite Nat2Z.inj_succ. unfold Z.succ.
     rewrite Z.add_comm. rewrite Qinv_plus_distr. reflexivity.
@@ -501,7 +496,7 @@ Lemma CRmorph_mult_inv : forall {R1 R2 : ConstructiveReals}
 Proof.
   intros. apply (CRmult_eq_reg_r (CR_of_Q R2 (Z.pos p # 1))).
   left. apply (CRle_lt_trans _ (CR_of_Q R2 0)).
-  apply CR_of_Q_zero. apply CR_of_Q_lt. reflexivity.
+  apply CRle_refl. apply CR_of_Q_lt. reflexivity.
   apply (CReq_trans _ (CRmorph f x)).
   - apply (CReq_trans
              _ (CRmorph f (CRmult R1 (CRmult R1 x (CR_of_Q R1 (1 # p)))
@@ -511,22 +506,22 @@ Proof.
              _ (CRmult R1 x (CRmult R1 (CR_of_Q R1 (1 # p))
                                     (CR_of_Q R1 (Z.pos p # 1))))).
     destruct (CRisRing R1). apply CReq_sym, Rmul_assoc.
-    apply (CReq_trans _ (CRmult R1 x (CRone R1))).
+    apply (CReq_trans _ (CRmult R1 x 1)).
     apply (Rmul_ext (CRisRingExt R1)). apply CReq_refl.
     apply (CReq_trans _ (CR_of_Q R1 ((1#p) * (Z.pos p # 1)))).
     apply CReq_sym, CR_of_Q_mult.
     apply (CReq_trans _ (CR_of_Q R1 1)).
-    apply CR_of_Q_morph. reflexivity. apply CR_of_Q_one.
+    apply CR_of_Q_morph. reflexivity. reflexivity.
     apply CRmult_1_r.
   - apply (CReq_trans
              _ (CRmult R2 (CRmorph f x)
                        (CRmult R2 (CR_of_Q R2 (1 # p)) (CR_of_Q R2 (Z.pos p # 1))))).
     2: apply (Rmul_assoc (CRisRing R2)).
-    apply (CReq_trans _ (CRmult R2 (CRmorph f x) (CRone R2))).
+    apply (CReq_trans _ (CRmult R2 (CRmorph f x) 1)).
     apply CReq_sym, CRmult_1_r.
     apply (Rmul_ext (CRisRingExt R2)). apply CReq_refl.
     apply (CReq_trans _ (CR_of_Q R2 1)).
-    apply CReq_sym, CR_of_Q_one.
+    reflexivity.
     apply (CReq_trans _ (CR_of_Q R2 ((1#p)*(Z.pos p # 1)))).
     apply CR_of_Q_morph. reflexivity. apply CR_of_Q_mult.
 Qed.
@@ -571,7 +566,7 @@ Qed.
 Lemma CRmorph_mult_pos_pos_le : forall {R1 R2 : ConstructiveReals}
                                   (f : @ConstructiveRealsMorphism R1 R2)
                                   (x y : CRcarrier R1),
-    CRlt R1 (CRzero R1) y
+    CRlt R1 0 y
     -> CRmult R2 (CRmorph f x) (CRmorph f y)
        <= CRmorph f (CRmult R1 x y).
 Proof.
@@ -590,20 +585,20 @@ Proof.
     apply Qlt_minus_iff in H1. rewrite H4 in H1. inversion H1. }
   destruct (CR_Q_dense R1 (CRplus R1 x (CR_of_Q R1 ((q-r) * (1#A)))) x)
     as [s [H4 H5]].
-  - apply (CRlt_le_trans _ (CRplus R1 x (CRzero R1))).
+  - apply (CRlt_le_trans _ (CRplus R1 x 0)).
     2: apply CRplus_0_r. apply CRplus_lt_compat_l.
     apply (CRplus_lt_reg_l R1 (CR_of_Q R1 ((r-q) * (1#A)))).
-    apply (CRle_lt_trans _ (CRzero R1)).
+    apply (CRle_lt_trans _ 0).
     apply (CRle_trans _ (CR_of_Q R1 ((r-q)*(1#A) + (q-r)*(1#A)))).
     destruct (CR_of_Q_plus R1 ((r-q)*(1#A)) ((q-r)*(1#A))).
     exact H0. apply (CRle_trans _ (CR_of_Q R1 0)).
-    2: destruct (@CR_of_Q_zero R1); exact H4.
+    2: apply CRle_refl.
     intro H4. apply lt_CR_of_Q in H4. ring_simplify in H4.
     inversion H4.
     apply (CRlt_le_trans _ (CR_of_Q R1 ((r - q) * (1 # A)))).
     2: apply CRplus_0_r.
     apply (CRle_lt_trans _ (CR_of_Q R1 0)).
-    apply CR_of_Q_zero. apply CR_of_Q_lt.
+    apply CRle_refl. apply CR_of_Q_lt.
     rewrite <- (Qmult_0_r (r-q)). apply Qmult_lt_l.
     apply Qlt_minus_iff in H1. exact H1. reflexivity.
   - apply (CRmorph_increasing f) in H4.
@@ -637,7 +632,7 @@ Proof.
       apply (CRlt_le_trans
                _ (CRmult R2 (CR_of_Q R2 ((q - r) * (1 # A))) (CRmorph f y))).
       apply (CRmult_lt_reg_l (CR_of_Q R2 (/((r-q)*(1#A))))).
-      apply (CRle_lt_trans _ (CR_of_Q R2 0)). apply CR_of_Q_zero.
+      apply (CRle_lt_trans _ (CR_of_Q R2 0)). apply CRle_refl.
       apply CR_of_Q_lt, Qinv_lt_0_compat.
       rewrite <- (Qmult_0_r (r-q)). apply Qmult_lt_l.
       apply Qlt_minus_iff in H1. exact H1. reflexivity.
@@ -655,24 +650,24 @@ Proof.
       apply (CRlt_le_trans _ (CRmorph f (CR_of_Q R1 (Z.pos A # 1)))).
       apply CRmorph_increasing. exact Amaj.
       destruct (CRmorph_rat f (Z.pos A # 1)). exact H4.
-      apply (CRle_trans _ (CRmult R2 (CRopp R2 (CRone R2)) (CRmorph f y))).
-      apply (CRle_trans _ (CRopp R2 (CRmult R2 (CRone R2) (CRmorph f y)))).
+      apply (CRle_trans _ (CRmult R2 (CRopp R2 1) (CRmorph f y))).
+      apply (CRle_trans _ (CRopp R2 (CRmult R2 1 (CRmorph f y)))).
       destruct (Ropp_ext (CRisRingExt R2) (CRmorph f y)
-                         (CRmult R2 (CRone R2) (CRmorph f y))).
+                         (CRmult R2 1 (CRmorph f y))).
       apply CReq_sym, (Rmul_1_l (CRisRing R2)). exact H4.
-      destruct (CRopp_mult_distr_l (CRone R2) (CRmorph f y)). exact H4.
+      destruct (CRopp_mult_distr_l 1 (CRmorph f y)). exact H4.
       apply (CRle_trans _ (CRmult R2 (CRmult R2 (CR_of_Q R2 (/ ((r - q) * (1 # A))))
                                              (CR_of_Q R2 ((q - r) * (1 # A))))
                                   (CRmorph f y))).
       apply CRmult_le_compat_r_half.
-      apply (CRle_lt_trans _ (CRmorph f (CRzero R1))).
+      apply (CRle_lt_trans _ (CRmorph f 0)).
       apply CRmorph_zero. apply CRmorph_increasing. exact H.
       apply (CRle_trans _ (CR_of_Q R2 ((/ ((r - q) * (1 # A)))
                                        * ((q - r) * (1 # A))))).
       apply (CRle_trans _ (CR_of_Q R2 (-1))).
       apply (CRle_trans _ (CRopp R2 (CR_of_Q R2 1))).
-      destruct (Ropp_ext (CRisRingExt R2) (CRone R2) (CR_of_Q R2 1)).
-      apply CReq_sym, CR_of_Q_one. exact H4.
+      destruct (Ropp_ext (CRisRingExt R2) 1 (CR_of_Q R2 1)).
+      reflexivity. exact H4.
       destruct (@CR_of_Q_opp R2 1). exact H0.
       destruct (CR_of_Q_morph R2 (-1) (/ ((r - q) * (1 # A)) * ((q - r) * (1 # A)))).
       field. split.
@@ -685,7 +680,7 @@ Proof.
                            (CRmorph f y)).
       exact H0.
       apply CRmult_le_compat_r_half.
-      apply (CRle_lt_trans _ (CRmorph f (CRzero R1))).
+      apply (CRle_lt_trans _ (CRmorph f 0)).
       apply CRmorph_zero. apply CRmorph_increasing. exact H.
       destruct (CRmorph_rat f ((q - r) * (1 # A))). exact H0.
     + apply (CRle_trans _ (CRmorph f (CRmult R1 y (CR_of_Q R1 s)))).
@@ -696,14 +691,14 @@ Proof.
       destruct (CRmorph_proper f (CRmult R1 y (CR_of_Q R1 s))
                                (CRmult R1 (CR_of_Q R1 s) y)).
       apply (Rmul_comm (CRisRing R1)). exact H4.
-    + apply (CRle_lt_trans _ (CRmorph f (CRzero R1))).
+    + apply (CRle_lt_trans _ (CRmorph f 0)).
       apply CRmorph_zero. apply CRmorph_increasing. exact H.
 Qed.
 
 Lemma CRmorph_mult_pos_pos : forall {R1 R2 : ConstructiveReals}
                                (f : @ConstructiveRealsMorphism R1 R2)
                                (x y : CRcarrier R1),
-    CRlt R1 (CRzero R1) y
+    CRlt R1 0 y
     -> CRmorph f (CRmult R1 x y)
        == CRmult R2 (CRmorph f x) (CRmorph f y).
 Proof.
@@ -718,10 +713,10 @@ Proof.
   destruct (CR_archimedean R1 y) as [A Amaj].
   destruct (CR_Q_dense R1 x (CRplus R1 x (CR_of_Q R1 ((q-r) * (1#A)))))
     as [s [H4 H5]].
-  - apply (CRle_lt_trans _ (CRplus R1 x (CRzero R1))).
+  - apply (CRle_lt_trans _ (CRplus R1 x 0)).
     apply CRplus_0_r. apply CRplus_lt_compat_l.
     apply (CRle_lt_trans _ (CR_of_Q R1 0)).
-    apply CR_of_Q_zero. apply CR_of_Q_lt.
+    apply CRle_refl. apply CR_of_Q_lt.
     rewrite <- (Qmult_0_r (q-r)). apply Qmult_lt_l.
     apply Qlt_minus_iff in H3. exact H3. reflexivity.
   - apply (CRmorph_increasing f) in H5.
@@ -763,14 +758,14 @@ Proof.
                          (CRmult R2 (CR_of_Q R2 ((q - r) * (1 # A)))
                                  (CRmorph f y)))).
       apply CRplus_le_compat_l, CRmult_le_compat_r_half.
-      apply (CRle_lt_trans _ (CRmorph f (CRzero R1))).
+      apply (CRle_lt_trans _ (CRmorph f 0)).
       apply CRmorph_zero. apply CRmorph_increasing. exact H.
       destruct (CRmorph_rat f ((q - r) * (1 # A))). exact H2.
       apply (CRlt_le_trans _ (CRplus R2 (CR_of_Q R2 r)
                                      (CR_of_Q R2 ((q - r))))).
       apply CRplus_lt_compat_l.
       * apply (CRmult_lt_reg_l (CR_of_Q R2 (/((q - r) * (1 # A))))).
-        apply (CRle_lt_trans _ (CR_of_Q R2 0)). apply CR_of_Q_zero.
+        apply (CRle_lt_trans _ (CR_of_Q R2 0)). apply CRle_refl.
         apply CR_of_Q_lt, Qinv_lt_0_compat.
         rewrite <- (Qmult_0_r (q-r)). apply Qmult_lt_l.
         apply Qlt_minus_iff in H3. exact H3. reflexivity.
@@ -781,9 +776,9 @@ Proof.
         exact (proj2 (Rmul_assoc (CRisRing R2) (CR_of_Q R2 (/ ((q - r) * (1 # A))))
                                  (CR_of_Q R2 ((q - r) * (1 # A)))
                                  (CRmorph f y))).
-        apply (CRle_trans _ (CRmult R2 (CRone R2) (CRmorph f y))).
+        apply (CRle_trans _ (CRmult R2 1 (CRmorph f y))).
         apply CRmult_le_compat_r_half.
-        apply (CRle_lt_trans _ (CRmorph f (CRzero R1))).
+        apply (CRle_lt_trans _ (CRmorph f 0)).
         apply CRmorph_zero. apply CRmorph_increasing. exact H.
         apply (CRle_trans
                  _ (CR_of_Q R2 ((/ ((q - r) * (1 # A))) * ((q - r) * (1 # A))))).
@@ -793,7 +788,7 @@ Proof.
         field_simplify. reflexivity. split.
         intro H5. inversion H5. intro H5. apply Qlt_minus_iff in H3.
         rewrite H5 in H3. inversion H3. exact H2.
-        destruct (CR_of_Q_one R2). exact H2.
+        apply CRle_refl.
         destruct (Rmul_1_l (CRisRing R2) (CRmorph f y)).
         intro H5. contradiction.
         apply (CRlt_le_trans _ (CR_of_Q R2 (Z.pos A # 1))).
@@ -809,7 +804,7 @@ Proof.
       * apply (CRle_trans _ (CR_of_Q R2 (r + (q-r)))).
         exact (proj1 (CR_of_Q_plus R2 r (q-r))).
         destruct (CR_of_Q_morph R2 (r + (q-r)) q). ring. exact H2.
-    + apply (CRle_lt_trans _ (CRmorph f (CRzero R1))).
+    + apply (CRle_lt_trans _ (CRmorph f 0)).
       apply CRmorph_zero. apply CRmorph_increasing. exact H.
 Qed.
 
@@ -867,10 +862,10 @@ Lemma CRmorph_appart_zero : forall {R1 R2 : ConstructiveReals}
     CRmorph f x ≶ 0.
 Proof.
   intros. destruct app.
-  - left. apply (CRlt_le_trans _ (CRmorph f (CRzero R1))).
+  - left. apply (CRlt_le_trans _ (CRmorph f 0)).
     apply CRmorph_increasing. exact c.
     exact (proj2 (CRmorph_zero f)).
-  - right. apply (CRle_lt_trans  _ (CRmorph f (CRzero R1))).
+  - right. apply (CRle_lt_trans  _ (CRmorph f 0)).
     exact (proj1 (CRmorph_zero f)).
     apply CRmorph_increasing. exact c.
 Defined.
@@ -885,7 +880,7 @@ Lemma CRmorph_inv : forall {R1 R2 : ConstructiveReals}
 Proof.
   intros. apply (CRmult_eq_reg_r (CRmorph f x)).
   destruct fxnz. right. exact c. left. exact c.
-  apply (CReq_trans _ (CRone R2)).
+  apply (CReq_trans _ 1).
   2: apply CReq_sym, CRinv_l.
   apply (CReq_trans _ (CRmorph f (CRmult R1 ((/ x) xnz) x))).
   apply CReq_sym, CRmorph_mult.
@@ -915,11 +910,11 @@ Proof.
   - simpl. unfold INR.
     rewrite (CRmorph_proper f _ (1 + CR_of_Q R1 (Z.of_nat n # 1))).
     rewrite CRmorph_plus. unfold INR in IHn.
-    rewrite IHn. rewrite CRmorph_one, <- CR_of_Q_one, <- CR_of_Q_plus.
+    rewrite IHn. rewrite CRmorph_one, <- CR_of_Q_plus.
     apply CR_of_Q_morph. rewrite Qinv_plus_distr.
     unfold Qeq, Qnum, Qden. do 2 rewrite Z.mul_1_r.
     rewrite Nat2Z.inj_succ. rewrite <- Z.add_1_l. reflexivity.
-    rewrite <- CR_of_Q_one, <- CR_of_Q_plus.
+    rewrite <- CR_of_Q_plus.
     apply CR_of_Q_morph. rewrite Qinv_plus_distr.
     unfold Qeq, Qnum, Qden. do 2 rewrite Z.mul_1_r.
     rewrite Nat2Z.inj_succ. rewrite <- Z.add_1_l. reflexivity.
@@ -1047,7 +1042,7 @@ Proof.
     apply Pos2Z.pos_le_pos, Pos2Nat.inj_le. rewrite Nat2Pos.id. exact H0.
     destruct i. inversion H0. pose proof (Pos2Nat.is_pos p).
     rewrite H2 in H1. inversion H1. discriminate.
-    rewrite <- CR_of_Q_zero. apply CR_of_Q_le. discriminate.
+    apply CR_of_Q_le. discriminate.
     rewrite CRplus_0_r. reflexivity. }
   pose proof (CR_cv_open_above _ _ _ H0 H) as [n nmaj].
   apply (CRle_lt_trans _ (CR_of_Q R2 (let (q0, _) := CR_Q_limit x n in
diff --git a/theories/Reals/Abstract/ConstructiveSum.v b/theories/Reals/Abstract/ConstructiveSum.v
index 11c8e5d8a2..3be03bf615 100644
--- a/theories/Reals/Abstract/ConstructiveSum.v
+++ b/theories/Reals/Abstract/ConstructiveSum.v
@@ -60,11 +60,11 @@ Lemma sum_const : forall {R : ConstructiveReals} (a : CRcarrier R) (n : nat),
     CRsum (fun _ => a) n == a * INR (S n).
 Proof.
   induction n.
-  - unfold INR. simpl. rewrite CR_of_Q_one, CRmult_1_r. reflexivity.
+  - unfold INR. simpl. rewrite CRmult_1_r. reflexivity.
   - simpl. rewrite IHn. unfold INR.
     replace (Z.of_nat (S (S n))) with (Z.of_nat (S n) + 1)%Z.
     rewrite <- Qinv_plus_distr, CR_of_Q_plus, CRmult_plus_distr_l.
-    apply CRplus_morph. reflexivity. rewrite CR_of_Q_one, CRmult_1_r. reflexivity.
+    apply CRplus_morph. reflexivity. rewrite CRmult_1_r. reflexivity.
     replace 1%Z with (Z.of_nat 1). rewrite <- Nat2Z.inj_add.
     apply f_equal. rewrite Nat.add_comm. reflexivity. reflexivity.
 Qed.
diff --git a/theories/Reals/Cauchy/ConstructiveRcomplete.v b/theories/Reals/Cauchy/ConstructiveRcomplete.v
index be844c413a..754f9be5fe 100644
--- a/theories/Reals/Cauchy/ConstructiveRcomplete.v
+++ b/theories/Reals/Cauchy/ConstructiveRcomplete.v
@@ -309,12 +309,11 @@ Definition CRealConstructive : ConstructiveReals
   := Build_ConstructiveReals
        CReal CRealLt CRealLtIsLinear CRealLtProp
        CRealLtEpsilon CRealLtForget CRealLtDisjunctEpsilon
-       (inject_Q 0) (inject_Q 1)
+       inject_Q inject_Q_lt lt_inject_Q
        CReal_plus CReal_opp CReal_mult
+       inject_Q_plus inject_Q_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
-       inject_Q inject_Q_plus inject_Q_mult
-       inject_Q_one inject_Q_lt lt_inject_Q
        CRealQ_dense Rup_pos CReal_abs CRealAbsLUB CRealComplete.