Merge PR #12288: Prove that classical reals implement constructive reals.

Reviewed-by: MSoegtropIMC
Reviewed-by: Zimmi48

16 files changed, 1607 insertions, 1218 deletions

diff --git a/doc/changelog/10-standard-library/12287-zero-of-Q.rst b/doc/changelog/10-standard-library/12287-zero-of-Q.rst
new file mode 100644
index 0000000000..ba2c74379b
--- /dev/null
+++ b/doc/changelog/10-standard-library/12287-zero-of-Q.rst
@@ -0,0 +1,4 @@
+- **Changed:**
+  Replace `CRzero` and `CRone` by `CR_of_Q 0` and `CR_of_Q 1` in `ConstructiveReals`
+  (`#12287 <https://github.com/coq/coq/pull/12287>`_,
+  by Vincent Semeria).
diff --git a/doc/changelog/10-standard-library/12288-constructive-experimental.rst b/doc/changelog/10-standard-library/12288-constructive-experimental.rst
new file mode 100644
index 0000000000..ec9b66bd7a
--- /dev/null
+++ b/doc/changelog/10-standard-library/12288-constructive-experimental.rst
@@ -0,0 +1,7 @@
+- **Changed:**
+  Split files `ConstructiveMinMax` and `ConstructivePower`.
+
+  .. warning:: The constructive reals modules are marked as experimental.
+
+  (`#12288 <https://github.com/coq/coq/pull/12288>`_,
+  by Vincent Semeria).
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 426f67eb53..1a02d6e65d 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -540,18 +540,15 @@ through the <tt>Require Import</tt> command.</p>
     Formalization of real numbers
   </dt>
   <dd>
+    <dl> 
+  <dt> <b>Classical Reals</b>:
+    Real numbers with excluded middle, total order and least upper bounds
+  </dt>
+  <dd>
     theories/Reals/Rdefinitions.v
-    theories/Reals/Cauchy/ConstructiveCauchyReals.v
-    theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v
-    theories/Reals/Cauchy/ConstructiveCauchyAbs.v
     theories/Reals/ClassicalDedekindReals.v
+    theories/Reals/ClassicalConstructiveReals.v
     theories/Reals/Raxioms.v
-    theories/Reals/Abstract/ConstructiveReals.v
-    theories/Reals/Abstract/ConstructiveRealsMorphisms.v
-    theories/Reals/Abstract/ConstructiveLUB.v
-    theories/Reals/Abstract/ConstructiveAbs.v
-    theories/Reals/Abstract/ConstructiveLimits.v
-    theories/Reals/Abstract/ConstructiveSum.v
     theories/Reals/RIneq.v
     theories/Reals/DiscrR.v
     theories/Reals/ROrderedType.v
@@ -597,7 +594,6 @@ through the <tt>Require Import</tt> command.</p>
     theories/Reals/Ranalysis5.v
     theories/Reals/Ranalysis_reg.v
     theories/Reals/Rcomplete.v
-    theories/Reals/Cauchy/ConstructiveRcomplete.v
     theories/Reals/RiemannInt.v
     theories/Reals/RiemannInt_SF.v
     theories/Reals/Rpow_def.v
@@ -617,6 +613,31 @@ through the <tt>Require Import</tt> command.</p>
     (theories/Reals/Reals.v)
     theories/Reals/Runcountable.v
   </dd>
+  <dt> <b>Abstract Constructive Reals</b>:
+    Interface of constructive reals, proof of equivalence of all implementations. EXPERIMENTAL 
+  </dt>
+  <dd>
+    theories/Reals/Abstract/ConstructiveReals.v
+    theories/Reals/Abstract/ConstructiveRealsMorphisms.v
+    theories/Reals/Abstract/ConstructiveLUB.v
+    theories/Reals/Abstract/ConstructiveAbs.v
+    theories/Reals/Abstract/ConstructiveLimits.v
+    theories/Reals/Abstract/ConstructiveMinMax.v
+    theories/Reals/Abstract/ConstructivePower.v
+    theories/Reals/Abstract/ConstructiveSum.v 
+  </dd>
+  <dt> <b>Constructive Cauchy Reals</b>:
+    Cauchy sequences of rational numbers, implementation of the interface. EXPERIMENTAL
+  </dt>
+  <dd>
+    theories/Reals/Cauchy/ConstructiveRcomplete.v
+    theories/Reals/Cauchy/ConstructiveCauchyReals.v
+    theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v
+    theories/Reals/Cauchy/ConstructiveCauchyAbs.v
+  </dd>
+
+  </dl>
+  </dd>
 
   <dt> <b>Program</b>:
     Support for dependently-typed programming
diff --git a/theories/Reals/Abstract/ConstructiveAbs.v b/theories/Reals/Abstract/ConstructiveAbs.v
index 31397cbddd..b6ceeef46a 100644
--- a/theories/Reals/Abstract/ConstructiveAbs.v
+++ b/theories/Reals/Abstract/ConstructiveAbs.v
@@ -17,7 +17,10 @@ Local Open Scope ConstructiveReals.
 
 (** Properties of constructive absolute value (defined in
     ConstructiveReals.CRabs).
-    Definition of minimum, maximum and their properties. *)
+    Definition of minimum, maximum and their properties.
+
+    WARNING: this file is experimental and likely to change in future releases.
+*)
 
 Instance CRabs_morph
   : forall {R : ConstructiveReals},
@@ -322,626 +325,3 @@ Proof.
     rewrite <- CRabs_opp in H.
     exact (CRle_trans _ _ _ (CRle_abs _) H).
 Qed.
-
-
-(* Minimum *)
-
-Definition CRmin {R : ConstructiveReals} (x y : CRcarrier R) : CRcarrier R
-  := (x + y - CRabs _ (y - x)) * CR_of_Q _ (1#2).
-
-Lemma CRmin_lt_r : forall {R : ConstructiveReals} (x y : CRcarrier R),
-    CRmin x y < y -> CRmin x y == x.
-Proof.
-  intros. unfold CRmin. unfold CRmin in H.
-  apply (CRmult_eq_reg_r (CR_of_Q R 2)).
-  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 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.
-  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
-    with signature (CReq R) ==> (CReq R) ==> (CReq R)
-      as CRmin_morph.
-Proof.
-  intros. unfold CRmin.
-  apply CRmult_morph. 2: reflexivity.
-  unfold CRminus.
-  rewrite H, H0. reflexivity.
-Qed.
-
-Instance CRmin_morphT
-  : forall {R : ConstructiveReals},
-    CMorphisms.Proper
-      (CMorphisms.respectful (CReq R) (CMorphisms.respectful (CReq R) (CReq R))) (@CRmin R).
-Proof.
-  intros R x y H z t H0.
-  rewrite H, H0. reflexivity.
-Qed.
-
-Lemma CRmin_l : forall {R : ConstructiveReals} (x y : CRcarrier R),
-    CRmin x y <= x.
-Proof.
-  intros. unfold CRmin.
-  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 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))).
-  rewrite CRplus_opp_l, CRplus_0_l.
-  rewrite (CRplus_comm x), CRplus_assoc, CRplus_opp_l, CRplus_0_r.
-  apply CRle_abs.
-Qed.
-
-Lemma CRmin_r : forall {R : ConstructiveReals} (x y : CRcarrier R),
-    CRmin x y <= y.
-Proof.
-  intros. unfold CRmin.
-  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 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)).
-  rewrite <- CRplus_assoc, CRplus_opp_l, CRplus_0_l.
-  rewrite <- (CRopp_involutive y), <- CRopp_plus_distr, <- CRopp_plus_distr.
-  apply CRopp_ge_le_contravar. rewrite CRabs_opp, CRplus_comm.
-  apply CRle_abs.
-Qed.
-
-Lemma CRnegPartAbsMin : forall {R : ConstructiveReals} (x : CRcarrier R),
-    CRmin 0 x == (x - CRabs _ x) * (CR_of_Q _ (1#2)).
-Proof.
-  intros. unfold CRmin. unfold CRminus. rewrite CRplus_0_l.
-  apply CRmult_morph. 2: reflexivity. rewrite CRopp_0, CRplus_0_r. reflexivity.
-Qed.
-
-Lemma CRmin_sym : forall {R : ConstructiveReals} (x y : CRcarrier R),
-    CRmin x y == CRmin y x.
-Proof.
-  intros. unfold CRmin. apply CRmult_morph. 2: reflexivity.
-  rewrite CRabs_minus_sym. unfold CRminus.
-  rewrite (CRplus_comm x y). reflexivity.
-Qed.
-
-Lemma CRmin_mult :
-  forall {R : ConstructiveReals} (p q r : CRcarrier R),
-    0 <= r -> CRmin (r * p) (r * q) == r * CRmin p q.
-Proof.
-  intros R p q r H. unfold CRmin.
-  setoid_replace (r * q - r * p) with (r * (q - p)).
-  rewrite CRabs_mult.
-  rewrite (CRabs_right r). 2: exact H.
-  rewrite <- CRmult_assoc. apply CRmult_morph. 2: reflexivity.
-  unfold CRminus. rewrite CRopp_mult_distr_r.
-  do 2 rewrite <- CRmult_plus_distr_l. reflexivity.
-  unfold CRminus. rewrite CRopp_mult_distr_r.
-  rewrite <- CRmult_plus_distr_l. reflexivity.
-Qed.
-
-Lemma CRmin_plus : forall {R : ConstructiveReals} (x y z : CRcarrier R),
-    x + CRmin y z == CRmin (x + y) (x + z).
-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. 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 CRmult_1_r.
-  rewrite CRmult_assoc, <- CR_of_Q_mult.
-  setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity.
-  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.
-  rewrite CRopp_plus_distr. rewrite <- CRplus_assoc.
-  apply CRplus_morph. 2: reflexivity.
-  rewrite CRplus_comm, <- CRplus_assoc, CRplus_opp_l.
-  apply CRplus_0_l.
-Qed.
-
-Lemma CRmin_left : forall {R : ConstructiveReals} (x y : CRcarrier R),
-    x <= y -> CRmin x y == x.
-Proof.
-  intros. unfold CRmin.
-  apply (CRmult_eq_reg_r (CR_of_Q R 2)).
-  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 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.
-  rewrite <- (CRplus_opp_r x). apply CRplus_le_compat.
-  exact H. apply CRle_refl.
-Qed.
-
-Lemma CRmin_right : forall {R : ConstructiveReals} (x y : CRcarrier R),
-    y <= x -> CRmin x y == y.
-Proof.
-  intros. unfold CRmin.
-  apply (CRmult_eq_reg_r (CR_of_Q R 2)).
-  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 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.
-  do 2 rewrite CRopp_involutive.
-  rewrite CRplus_comm, CRplus_assoc, CRplus_opp_l, CRplus_0_r. reflexivity.
-  rewrite <- (CRplus_opp_r x). apply CRplus_le_compat.
-  exact H. apply CRle_refl.
-Qed.
-
-Lemma CRmin_lt : forall {R : ConstructiveReals} (x y z : CRcarrier R),
-    z < x -> z < y -> z < CRmin x y.
-Proof.
-  intros. unfold CRmin.
-  apply (CRmult_lt_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 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))).
-  rewrite (CRplus_comm (x+y)), CRplus_assoc.
-  rewrite <- (CRplus_assoc (CRabs R (y + - x))), CRplus_opp_r, CRplus_0_l.
-  rewrite <- (CRplus_comm (x+y)).
-  apply CRabs_def1.
-  - unfold CRminus. rewrite <- (CRplus_comm y), CRplus_assoc.
-    apply CRplus_lt_compat_l.
-    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), CRmult_plus_distr_l.
-    rewrite CRmult_1_r. apply CRplus_le_lt_compat.
-    apply CRlt_asym.
-    apply CRopp_gt_lt_contravar, H.
-    apply CRopp_gt_lt_contravar, H.
-  - rewrite CRopp_plus_distr, CRopp_involutive.
-    rewrite CRplus_comm, CRplus_assoc.
-    apply CRplus_lt_compat_l.
-    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), CRmult_plus_distr_l.
-    rewrite CRmult_1_r. apply CRplus_le_lt_compat.
-    apply CRlt_asym.
-    apply CRopp_gt_lt_contravar, H0.
-    apply CRopp_gt_lt_contravar, H0.
-Qed.
-
-Lemma CRmin_contract : forall {R : ConstructiveReals} (x y a : CRcarrier R),
-    CRabs _ (CRmin x a - CRmin y a) <= CRabs _ (x - y).
-Proof.
-  intros. unfold CRmin.
-  unfold CRminus. rewrite CRopp_mult_distr_l, <- CRmult_plus_distr_r.
-  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: 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.
-  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.
-  rewrite (CRabs_morph (x-y) ((a-y)-(a-x))).
-  apply CRabs_triang_inv2.
-  unfold CRminus. rewrite (CRplus_comm (a + - y)).
-  rewrite <- CRplus_assoc. apply CRplus_morph. 2: reflexivity.
-  rewrite CRplus_comm, CRopp_plus_distr, <- CRplus_assoc.
-  rewrite CRplus_opp_r, CRopp_involutive, CRplus_0_l.
-  reflexivity.
-  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 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.
-  rewrite CRplus_assoc. apply CRplus_morph. reflexivity.
-  rewrite CRopp_plus_distr. rewrite (CRplus_comm (-a)).
-  rewrite CRplus_assoc, <- (CRplus_assoc (-a)), CRplus_opp_l.
-  rewrite CRplus_0_l, CRopp_involutive. reflexivity.
-Qed.
-
-Lemma CRmin_glb : forall {R : ConstructiveReals} (x y z:CRcarrier R),
-    z <= x -> z <= y -> z <= CRmin x y.
-Proof.
-  intros. unfold CRmin.
-  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 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))).
-  rewrite CRplus_assoc, <- (CRplus_assoc (- CRabs R (y + - x))).
-  rewrite CRplus_opp_l, CRplus_0_l.
-  apply CRabs_le. split.
-  - do 2 rewrite CRopp_plus_distr.
-    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), 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), CRmult_plus_distr_l.
-    rewrite CRmult_1_r.
-    apply CRplus_le_compat; apply CRopp_ge_le_contravar; exact H.
-Qed.
-
-Lemma CRmin_assoc : forall {R : ConstructiveReals} (a b c : CRcarrier R),
-    CRmin a (CRmin b c) == CRmin (CRmin a b) c.
-Proof.
-  split.
-  - apply CRmin_glb.
-    + apply (CRle_trans _ (CRmin a b)).
-      apply CRmin_l. apply CRmin_l.
-    + apply CRmin_glb.
-      apply (CRle_trans _ (CRmin a b)).
-      apply CRmin_l. apply CRmin_r. apply CRmin_r.
-  - apply CRmin_glb.
-    + apply CRmin_glb. apply CRmin_l.
-      apply (CRle_trans _ (CRmin b c)).
-      apply CRmin_r. apply CRmin_l.
-    + apply (CRle_trans _ (CRmin b c)).
-      apply CRmin_r. apply CRmin_r.
-Qed.
-
-Lemma CRlt_min : forall {R : ConstructiveReals} (x y z : CRcarrier R),
-    z < CRmin x y -> prod (z < x) (z < y).
-Proof.
-  intros. destruct (CR_Q_dense R _ _ H) as [q qmaj].
-  destruct qmaj.
-  split.
-  - apply (CRlt_le_trans _ (CR_of_Q R q) _ c).
-    intro abs. apply (CRlt_asym _ _ c0).
-    apply (CRle_lt_trans _ x). apply CRmin_l. exact abs.
-  - apply (CRlt_le_trans _ (CR_of_Q R q) _ c).
-    intro abs. apply (CRlt_asym _ _ c0).
-    apply (CRle_lt_trans _ y). apply CRmin_r. exact abs.
-Qed.
-
-
-
-(* Maximum *)
-
-Definition CRmax {R : ConstructiveReals} (x y : CRcarrier R) : CRcarrier R
-  := (x + y + CRabs _ (y - x)) * CR_of_Q _ (1#2).
-
-Add Parametric Morphism {R : ConstructiveReals} : CRmax
-    with signature (CReq R) ==> (CReq R) ==> (CReq R)
-      as CRmax_morph.
-Proof.
-  intros. unfold CRmax.
-  apply CRmult_morph. 2: reflexivity. unfold CRminus.
-  rewrite H, H0. reflexivity.
-Qed.
-
-Instance CRmax_morphT
-  : forall {R : ConstructiveReals},
-    CMorphisms.Proper
-      (CMorphisms.respectful (CReq R) (CMorphisms.respectful (CReq R) (CReq R))) (@CRmax R).
-Proof.
-  intros R x y H z t H0.
-  rewrite H, H0. reflexivity.
-Qed.
-
-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)).
-  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 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.
-  apply CRabs_le. split.
-  - repeat rewrite CRopp_plus_distr.
-    do 2 rewrite CRopp_involutive.
-    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, 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, CRmult_1_r.
-    apply CRplus_le_compat; assumption.
-Qed.
-
-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)).
-  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 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)).
-  rewrite <- CRplus_assoc, CRplus_opp_l, CRplus_0_l.
-  rewrite CRabs_minus_sym, CRplus_comm.
-  apply CRle_abs. reflexivity.
-Qed.
-
-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)).
-  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 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)).
-  rewrite <- CRplus_assoc, CRplus_opp_l, CRplus_0_l.
-  rewrite CRplus_comm. apply CRle_abs.
-Qed.
-
-Lemma CRposPartAbsMax : forall {R : ConstructiveReals} (x : CRcarrier R),
-    CRmax 0 x == (x + CRabs _ x) * (CR_of_Q R (1#2)).
-Proof.
-  intros. unfold CRmax. unfold CRminus. rewrite CRplus_0_l.
-  apply CRmult_morph. 2: reflexivity. rewrite CRopp_0, CRplus_0_r. reflexivity.
-Qed.
-
-Lemma CRmax_sym : forall {R : ConstructiveReals} (x y : CRcarrier R),
-    CRmax x y == CRmax y x.
-Proof.
-  intros. unfold CRmax.
-  rewrite CRabs_minus_sym. apply CRmult_morph.
-  2: reflexivity. rewrite (CRplus_comm x y). reflexivity.
-Qed.
-
-Lemma CRmax_plus : forall {R : ConstructiveReals} (x y z : CRcarrier R),
-    x + CRmax y z == CRmax (x + y) (x + z).
-Proof.
-  intros. unfold CRmax.
-  setoid_replace (x + z - (x + y)) with (z-y).
-  apply (CRmult_eq_reg_r (CR_of_Q _ 2)).
-  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 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, 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.
-  rewrite (CRplus_comm x). apply CRplus_assoc.
-  unfold CRminus. rewrite CRopp_plus_distr. rewrite <- CRplus_assoc.
-  apply CRplus_morph. 2: reflexivity.
-  rewrite CRplus_comm, <- CRplus_assoc, CRplus_opp_l.
-  apply CRplus_0_l.
-Qed.
-
-Lemma CRmax_left : forall {R : ConstructiveReals} (x y : CRcarrier R),
-    y <= x -> CRmax x y == x.
-Proof.
-  intros. unfold CRmax.
-  apply (CRmult_eq_reg_r (CR_of_Q R 2)).
-  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 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.
-  rewrite <- (CRplus_opp_r x). apply CRplus_le_compat_r. exact H.
-Qed.
-
-Lemma CRmax_right : forall {R : ConstructiveReals} (x y : CRcarrier R),
-    x <= y -> CRmax x y == y.
-Proof.
-  intros. unfold CRmax.
-  apply (CRmult_eq_reg_r (CR_of_Q R 2)).
-  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 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.
-  rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r. reflexivity.
-  rewrite <- (CRplus_opp_r x). apply CRplus_le_compat_r. exact H.
-Qed.
-
-Lemma CRmax_contract : forall {R : ConstructiveReals} (x y a : CRcarrier R),
-    CRabs _ (CRmax x a - CRmax y a) <= CRabs _ (x - y).
-Proof.
-  intros. unfold CRmax.
-  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: 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.
-  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.
-  rewrite (CRabs_minus_sym x y).
-  rewrite (CRabs_morph (y-x) ((a-x)-(a-y))).
-  apply CRabs_triang_inv2.
-  unfold CRminus. rewrite (CRplus_comm (a + - x)).
-  rewrite <- CRplus_assoc. apply CRplus_morph. 2: reflexivity.
-  rewrite CRplus_comm, CRopp_plus_distr, <- CRplus_assoc.
-  rewrite CRplus_opp_r, CRopp_involutive, CRplus_0_l.
-  reflexivity.
-  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 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.
-  rewrite <- CRplus_assoc. rewrite CRplus_comm, CRopp_plus_distr.
-  rewrite CRplus_assoc. apply CRplus_morph. reflexivity.
-  rewrite CRopp_plus_distr. rewrite (CRplus_comm (-a)).
-  rewrite CRplus_assoc, <- (CRplus_assoc (-a)), CRplus_opp_l.
-  rewrite CRplus_0_l. apply CRplus_comm.
-Qed.
-
-Lemma CRmax_lub_lt : forall {R : ConstructiveReals} (x y z : CRcarrier R),
-    x < z -> y < z -> CRmax x y < z.
-Proof.
-  intros. unfold CRmax.
-  apply (CRmult_lt_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 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.
-  apply CRabs_def1.
-  - rewrite (CRplus_comm y), (CRplus_comm (-y)), CRplus_assoc.
-    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), 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), CRmult_plus_distr_l.
-    rewrite CRmult_1_r. apply CRplus_le_lt_compat.
-    apply CRlt_asym, H. exact H.
-Qed.
-
-Lemma CRmax_assoc : forall {R : ConstructiveReals} (a b c : CRcarrier R),
-    CRmax a (CRmax b c) == CRmax (CRmax a b) c.
-Proof.
-  split.
-  - apply CRmax_lub.
-    + apply CRmax_lub. apply CRmax_l.
-      apply (CRle_trans _ (CRmax b c)).
-      apply CRmax_l. apply CRmax_r.
-    + apply (CRle_trans _ (CRmax b c)).
-      apply CRmax_r. apply CRmax_r.
-  - apply CRmax_lub.
-    + apply (CRle_trans _ (CRmax a b)).
-      apply CRmax_l. apply CRmax_l.
-    + apply CRmax_lub.
-      apply (CRle_trans _ (CRmax a b)).
-      apply CRmax_r. apply CRmax_l. apply CRmax_r.
-Qed.
-
-Lemma CRmax_min_mult_neg :
-  forall {R : ConstructiveReals} (p q r:CRcarrier R),
-    r <= 0 -> CRmax (r * p) (r * q) == r * CRmin p q.
-Proof.
-  intros R p q r H. unfold CRmin, CRmax.
-  setoid_replace (r * q - r * p) with (r * (q - p)).
-  rewrite CRabs_mult.
-  rewrite (CRabs_left r), <- CRmult_assoc.
-  apply CRmult_morph. 2: reflexivity. unfold CRminus.
-  rewrite <- CRopp_mult_distr_l, CRopp_mult_distr_r,
-  CRmult_plus_distr_l, CRmult_plus_distr_l.
-  reflexivity. exact H.
-  unfold CRminus. rewrite CRmult_plus_distr_l, CRopp_mult_distr_r. reflexivity.
-Qed.
-
-Lemma CRlt_max : forall {R : ConstructiveReals} (x y z : CRcarrier R),
-    CRmax x y < z -> prod (x < z) (y < z).
-Proof.
-  intros. destruct (CR_Q_dense R _ _ H) as [q qmaj].
-  destruct qmaj.
-  split.
-  - apply (CRlt_le_trans _ (CR_of_Q R q)).
-    apply (CRle_lt_trans _ (CRmax x y)). apply CRmax_l. exact c.
-    apply CRlt_asym, c0.
-  - apply (CRlt_le_trans _ (CR_of_Q R q)).
-    apply (CRle_lt_trans _ (CRmax x y)). apply CRmax_r. exact c.
-    apply CRlt_asym, c0.
-Qed.
-
-Lemma CRmax_mult :
-  forall {R : ConstructiveReals} (p q r:CRcarrier R),
-    0 <= r -> CRmax (r * p) (r * q) == r * CRmax p q.
-Proof.
-  intros R p q r H. unfold CRmin, CRmax.
-  setoid_replace (r * q - r * p) with (r * (q - p)).
-  rewrite CRabs_mult.
-  rewrite (CRabs_right r), <- CRmult_assoc.
-  apply CRmult_morph. 2: reflexivity.
-  rewrite CRmult_plus_distr_l, CRmult_plus_distr_l.
-  reflexivity. exact H.
-  unfold CRminus. rewrite CRmult_plus_distr_l, CRopp_mult_distr_r. reflexivity.
-Qed.
-
-Lemma CRmin_max_mult_neg :
-  forall {R : ConstructiveReals} (p q r:CRcarrier R),
-    r <= 0 -> CRmin (r * p) (r * q) == r * CRmax p q.
-Proof.
-  intros R p q r H. unfold CRmin, CRmax.
-  setoid_replace (r * q - r * p) with (r * (q - p)).
-  rewrite CRabs_mult.
-  rewrite (CRabs_left r), <- CRmult_assoc.
-  apply CRmult_morph. 2: reflexivity. unfold CRminus.
-  rewrite CRopp_mult_distr_l, CRopp_involutive,
-  CRmult_plus_distr_l, CRmult_plus_distr_l.
-  reflexivity. exact H.
-  unfold CRminus. rewrite CRmult_plus_distr_l, CRopp_mult_distr_r. reflexivity.
-Qed.
diff --git a/theories/Reals/Abstract/ConstructiveLUB.v b/theories/Reals/Abstract/ConstructiveLUB.v
index 1c19c6aa40..883bb50634 100644
--- a/theories/Reals/Abstract/ConstructiveLUB.v
+++ b/theories/Reals/Abstract/ConstructiveLUB.v
@@ -11,7 +11,10 @@
 
 (** 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. *)
+    subsets of the real numbers.
+
+   WARNING: this file is experimental and likely to change in future releases.
+*)
 
 Require Import QArith_base Qabs.
 Require Import ConstructiveReals.
diff --git a/theories/Reals/Abstract/ConstructiveLimits.v b/theories/Reals/Abstract/ConstructiveLimits.v
index 64dcd2e1ec..6fe4d4ca3f 100644
--- a/theories/Reals/Abstract/ConstructiveLimits.v
+++ b/theories/Reals/Abstract/ConstructiveLimits.v
@@ -11,13 +11,15 @@
 Require Import QArith Qabs.
 Require Import ConstructiveReals.
 Require Import ConstructiveAbs.
-Require Import ConstructiveSum.
 
 Local Open Scope ConstructiveReals.
 
 
 (** Definitions and basic properties of limits of real sequences
-    and series. *)
+    and series.
+
+    WARNING: this file is experimental and likely to change in future releases.
+*)
 
 
 Lemma CR_cv_extens
@@ -219,18 +221,6 @@ Proof.
   exists p. intros. apply CRlt_asym. apply pmaj. apply H.
 Qed.
 
-Definition series_cv {R : ConstructiveReals}
-           (un : nat -> CRcarrier R) (s : CRcarrier R) : Set
-  := CR_cv R (CRsum un) s.
-
-Definition series_cv_lim_lt {R : ConstructiveReals}
-           (un : nat -> CRcarrier R) (x : CRcarrier R) : Set
-  := { l : CRcarrier R & prod (series_cv un l) (l < x) }.
-
-Definition series_cv_le_lim {R : ConstructiveReals}
-           (x : CRcarrier R) (un : nat -> CRcarrier R) : Set
-  := { l : CRcarrier R & prod (series_cv un l) (x <= l) }.
-
 Lemma CR_cv_minus :
   forall {R : ConstructiveReals}
     (An Bn:nat -> CRcarrier R) (l1 l2:CRcarrier R),
@@ -260,13 +250,6 @@ Proof.
   rewrite CRplus_0_l. exact H1.
 Qed.
 
-Lemma series_cv_unique :
-  forall {R : ConstructiveReals} (Un:nat -> CRcarrier R) (l1 l2:CRcarrier R),
-    series_cv Un l1 -> series_cv Un l2 -> l1 == l2.
-Proof.
-  intros. apply (CR_cv_unique (CRsum Un)); assumption.
-Qed.
-
 Lemma CR_cv_scale : forall {R : ConstructiveReals} (u : nat -> CRcarrier R)
                       (a : CRcarrier R) (s : CRcarrier R),
     CR_cv R u s -> CR_cv R (fun n => u n * a) (s * a).
@@ -328,17 +311,6 @@ Proof.
   - rewrite Qinv_plus_distr. reflexivity.
 Qed.
 
-Lemma series_cv_eq : forall {R : ConstructiveReals}
-                       (u v : nat -> CRcarrier R) (s : CRcarrier R),
-    (forall n:nat, u n == v n)
-    -> series_cv u s
-    -> series_cv v s.
-Proof.
-  intros. intros p. specialize (H0 p). destruct H0 as [N H0].
-  exists N. intros. unfold CRminus.
-  rewrite <- (CRsum_eq u). apply H0, H1. intros. apply H.
-Qed.
-
 Lemma CR_growing_transit : forall {R : ConstructiveReals} (un : nat -> CRcarrier R),
     (forall n:nat, un n <= un (S n))
     -> forall n p : nat, le n p -> un n <= un p.
@@ -439,135 +411,6 @@ Proof.
     apply Nat.add_le_mono_l. apply le_0_n.
 Qed.
 
-Lemma series_cv_maj : forall {R : ConstructiveReals}
-                        (un vn : nat -> CRcarrier R) (s : CRcarrier R),
-    (forall n:nat, CRabs R (un n) <= vn n)
-    -> series_cv vn s
-    -> { l : CRcarrier R & prod (series_cv un l) (l <= s) }.
-Proof.
-  intros. destruct (CR_complete R (CRsum un)).
-  - intros n.
-    specialize (H0 (2*n)%positive) as [N maj].
-    exists N. intros i j H0 H1.
-    apply (CRle_trans _ (CRsum vn (max i j) - CRsum vn (min i j))).
-    apply Abs_sum_maj. apply H.
-    setoid_replace (CRsum vn (max i j) - CRsum vn (min i j))
-      with (CRabs R (CRsum vn (max i j) - (CRsum vn (min i j)))).
-    setoid_replace (CRsum vn (Init.Nat.max i j) - CRsum vn (Init.Nat.min i j))
-      with (CRsum vn (Init.Nat.max i j) - s - (CRsum vn (Init.Nat.min i j) - s)).
-    apply (CRle_trans _ _ _ (CRabs_triang _ _)).
-    setoid_replace (1#n)%Q with ((1#2*n) + (1#2*n))%Q.
-    rewrite CR_of_Q_plus.
-    apply CRplus_le_compat.
-    apply maj. apply (le_trans _ i). assumption. apply Nat.le_max_l.
-    rewrite CRabs_opp. apply maj.
-    apply Nat.min_case. apply (le_trans _ i). assumption. apply le_refl.
-    assumption. rewrite Qinv_plus_distr. reflexivity.
-    unfold CRminus. rewrite CRplus_assoc. apply CRplus_morph.
-    reflexivity. rewrite CRopp_plus_distr, CRopp_involutive.
-    rewrite CRplus_comm, CRplus_assoc, CRplus_opp_r, CRplus_0_r.
-    reflexivity.
-    rewrite CRabs_right. reflexivity.
-    rewrite <- (CRplus_opp_r (CRsum vn (Init.Nat.min i j))).
-    apply CRplus_le_compat. apply pos_sum_more.
-    intros. apply (CRle_trans _ (CRabs R (un k))). apply CRabs_pos.
-    apply H. apply (le_trans _ i). apply Nat.le_min_l. apply Nat.le_max_l.
-    apply CRle_refl.
-  - exists x. split. assumption.
-    (* x <= s *)
-    apply (CRplus_le_reg_r (-x)). rewrite CRplus_opp_r.
-    apply (CR_cv_bound_down (fun n => CRsum vn n - CRsum un n) _ _ 0).
-    intros. rewrite <- (CRplus_opp_r (CRsum un n)).
-    apply CRplus_le_compat. apply sum_Rle.
-    intros. apply (CRle_trans _ (CRabs R (un k))).
-    apply CRle_abs. apply H. apply CRle_refl.
-    apply CR_cv_plus. assumption.
-    apply CR_cv_opp. assumption.
-Qed.
-
-Lemma series_cv_abs_lt
-  : forall {R : ConstructiveReals} (un vn : nat -> CRcarrier R) (l : CRcarrier R),
-    (forall n:nat, CRabs R (un n) <= vn n)
-    -> series_cv_lim_lt vn l
-    -> series_cv_lim_lt un l.
-Proof.
-  intros. destruct H0 as [x [H0 H1]].
-  destruct (series_cv_maj un vn x H H0) as [x0 H2].
-  exists x0. split. apply H2. apply (CRle_lt_trans _ x).
-  apply H2. apply H1.
-Qed.
-
-Definition series_cv_abs {R : ConstructiveReals} (u : nat -> CRcarrier R)
-  : CR_cauchy R (CRsum (fun n => CRabs R (u n)))
-    -> { l : CRcarrier R & series_cv u l }.
-Proof.
-  intros. apply CR_complete in H. destruct H.
-  destruct (series_cv_maj u (fun k => CRabs R (u k)) x).
-  intro n. apply CRle_refl. assumption. exists x0. apply p.
-Qed.
-
-Lemma series_cv_abs_eq
-  : forall {R : ConstructiveReals} (u : nat -> CRcarrier R) (a : CRcarrier R)
-           (cau : CR_cauchy R (CRsum (fun n => CRabs R (u n)))),
-    series_cv u a
-    -> (a == (let (l,_):= series_cv_abs u cau in l))%ConstructiveReals.
-Proof.
-  intros. destruct (series_cv_abs u cau).
-  apply (series_cv_unique u). exact H. exact s.
-Qed.
-
-Lemma series_cv_abs_cv
-  : forall {R : ConstructiveReals} (u : nat -> CRcarrier R)
-           (cau : CR_cauchy R (CRsum (fun n => CRabs R (u n)))),
-    series_cv u (let (l,_):= series_cv_abs u cau in l).
-Proof.
-  intros. destruct (series_cv_abs u cau). exact s.
-Qed.
-
-Lemma series_cv_opp : forall {R : ConstructiveReals}
-                        (s : CRcarrier R) (u : nat -> CRcarrier R),
-    series_cv u s
-    -> series_cv (fun n => - u n) (- s).
-Proof.
-  intros. intros p. specialize (H p) as [N H].
-  exists N. intros n H0.
-  setoid_replace (CRsum (fun n0 : nat => - u n0) n - - s)
-    with (-(CRsum (fun n0 : nat => u n0) n - s)).
-  rewrite CRabs_opp.
-  apply H, H0. unfold CRminus.
-  rewrite sum_opp. rewrite CRopp_plus_distr. reflexivity.
-Qed.
-
-Lemma series_cv_scale : forall {R : ConstructiveReals}
-                          (a : CRcarrier R) (s : CRcarrier R) (u : nat -> CRcarrier R),
-    series_cv u s
-    -> series_cv (fun n => (u n) * a) (s * a).
-Proof.
-  intros.
-  apply (CR_cv_eq _ (fun n => CRsum u n * a)).
-  intro n. rewrite sum_scale. reflexivity. apply CR_cv_scale, H.
-Qed.
-
-Lemma series_cv_plus : forall {R : ConstructiveReals}
-                         (u v : nat -> CRcarrier R) (s t : CRcarrier R),
-    series_cv u s
-    -> series_cv v t
-    -> series_cv (fun n => u n + v n) (s + t).
-Proof.
-  intros. apply (CR_cv_eq _ (fun n => CRsum u n + CRsum v n)).
-  intro n. symmetry. apply sum_plus. apply CR_cv_plus. exact H. exact H0.
-Qed.
-
-Lemma series_cv_nonneg : forall {R : ConstructiveReals}
-                           (u : nat -> CRcarrier R) (s : CRcarrier R),
-    (forall n:nat, 0 <= u n) -> series_cv u s -> 0 <= s.
-Proof.
-  intros. apply (CRle_trans 0 (CRsum u 0)). apply H.
-  apply (growing_ineq (CRsum u)). intro n. simpl.
-  rewrite <- CRplus_0_r. apply CRplus_le_compat.
-  rewrite CRplus_0_r. apply CRle_refl. apply H. apply H0.
-Qed.
-
 Lemma CR_cv_le : forall {R : ConstructiveReals}
                    (u v : nat -> CRcarrier R) (a b : CRcarrier R),
     (forall n:nat, u n <= v n)
@@ -612,251 +455,6 @@ Proof.
   rewrite <- CRplus_assoc, CRplus_opp_r, CRplus_0_l. reflexivity.
 Qed.
 
-Lemma series_cv_triangle : forall {R : ConstructiveReals}
-                             (u : nat -> CRcarrier R) (s sAbs : CRcarrier R),
-    series_cv u s
-    -> series_cv (fun n => CRabs R (u n)) sAbs
-    -> CRabs R s <= sAbs.
-Proof.
-  intros.
-  apply (CR_cv_le (fun n => CRabs R (CRsum u n))
-                   (CRsum (fun n => CRabs R (u n)))).
-  intros. apply multiTriangleIneg. apply CR_cv_abs_cont. assumption. assumption.
-Qed.
-
-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.
-  rewrite CRmult_plus_distr_r, CRmult_1_l. reflexivity.
-Qed.
-
-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.
-    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))).
-    2: symmetry; apply Qinv_plus_distr.
-    rewrite CR_of_Q_plus.
-    replace (CRpow (CR_of_Q R 2) (1 + n))
-      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.
-    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; apply CR_of_Q_le; discriminate.
-  apply CRlt_asym.
-  apply (CRmult_lt_reg_l (CR_of_Q R (Z.pos p # 1))).
-  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.
-  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, 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.
-  reflexivity. reflexivity.
-Qed.
-
-Lemma GeoFiniteSum : forall {R : ConstructiveReals} (n:nat),
-    CRsum (CRpow (CR_of_Q R (1#2))) n == CR_of_Q R 2 - CRpow (CR_of_Q R (1#2)) n.
-Proof.
-  induction n.
-  - unfold CRsum, CRpow. simpl (1%ConstructiveReals).
-    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.
-    rewrite IHn. clear IHn. unfold CRminus.
-    rewrite CRplus_assoc. apply CRplus_morph. reflexivity.
-    apply (CRplus_eq_reg_l
-             (CRpow (CR_of_Q R (1 # 2)) n + CRpow (CR_of_Q R (1 # 2)) (S n))).
-    rewrite (CRplus_assoc _ _ (-CRpow (CR_of_Q R (1 # 2)) (S n))),
-    CRplus_opp_r, CRplus_0_r.
-    rewrite (CRplus_comm (CRpow (CR_of_Q R (1 # 2)) n)), CRplus_assoc.
-    rewrite <- (CRplus_assoc (CRpow (CR_of_Q R (1 # 2)) n)), CRplus_opp_r,
-    CRplus_0_l, <- CR_double.
-    setoid_replace (CRpow (CR_of_Q R (1 # 2)) (S n))
-      with (CR_of_Q R (1 # 2) * CRpow (CR_of_Q R (1 # 2)) n).
-    2: reflexivity.
-    rewrite <- CRmult_assoc, <- CR_of_Q_mult.
-    setoid_replace (2 * (1 # 2))%Q with 1%Q.
-    apply CRmult_1_l. reflexivity.
-Qed.
-
-Lemma GeoHalfBelowTwo : forall {R : ConstructiveReals} (n:nat),
-    CRsum (CRpow (CR_of_Q R (1#2))) n < CR_of_Q R 2.
-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. apply CR_of_Q_lt. reflexivity.
-Qed.
-
-Lemma GeoHalfTwo : forall {R : ConstructiveReals},
-    series_cv (fun n => CRpow (CR_of_Q R (1#2)) n) (CR_of_Q R 2).
-Proof.
-  intro R.
-  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.
-      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.
-      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. 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).
-    { 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))).
-    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 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).
-    rewrite H3 in H2. inversion H2.
-    apply Pos2Z.pos_le_pos. apply Pos2Nat.inj_le.
-    apply (le_trans _ _ _ H0). rewrite SuccNat2Pos.id_succ. apply le_refl.
-    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.
-    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.
-Qed.
-
-Lemma series_cv_remainder_maj : forall {R : ConstructiveReals} (u : nat -> CRcarrier R)
-                                  (s eps : CRcarrier R)
-                                  (N : nat),
-    series_cv u s
-    -> 0 < eps
-    -> (forall n:nat, 0 <= u n)
-    -> CRabs R (CRsum u N - s) <= eps
-    -> forall n:nat, CRsum (fun k=> u (N + S k)%nat) n <= eps.
-Proof.
-  intros. pose proof (sum_assoc u N n).
-  rewrite <- (CRsum_eq (fun k : nat => u (S N + k)%nat)).
-  apply (CRplus_le_reg_l (CRsum u N)). rewrite <- H3.
-  apply (CRle_trans _ s). apply growing_ineq.
-  2: apply H.
-  intro k. simpl. rewrite <- CRplus_0_r, CRplus_assoc.
-  apply CRplus_le_compat_l. rewrite CRplus_0_l. apply H1.
-  rewrite CRabs_minus_sym in H2.
-  rewrite CRplus_comm. apply (CRplus_le_reg_r (-CRsum u N)).
-  rewrite CRplus_assoc. rewrite CRplus_opp_r. rewrite CRplus_0_r.
-  apply (CRle_trans _ (CRabs R (s - CRsum u N))). apply CRle_abs.
-  assumption. intros. rewrite Nat.add_succ_r. reflexivity.
-Qed.
-
-Lemma series_cv_abs_remainder : forall {R : ConstructiveReals} (u : nat -> CRcarrier R)
-                                  (s sAbs : CRcarrier R)
-                                  (n : nat),
-    series_cv u s
-    -> series_cv (fun n => CRabs R (u n)) sAbs
-    -> CRabs R (CRsum u n - s)
-      <= sAbs - CRsum (fun n => CRabs R (u n)) n.
-Proof.
-  intros.
-  apply (CR_cv_le (fun N => CRabs R (CRsum u n - (CRsum u (n + N))))
-                   (fun N => CRsum (fun n : nat => CRabs R (u n)) (n + N)
-                          - CRsum (fun n : nat => CRabs R (u n)) n)).
-  - intro N. destruct N. rewrite plus_0_r. unfold CRminus.
-    rewrite CRplus_opp_r. rewrite CRplus_opp_r.
-    rewrite CRabs_right. apply CRle_refl. apply CRle_refl.
-    rewrite Nat.add_succ_r.
-    replace (S (n + N)) with (S n + N)%nat. 2: reflexivity.
-    unfold CRminus. rewrite sum_assoc. rewrite sum_assoc.
-    rewrite CRopp_plus_distr.
-    rewrite <- CRplus_assoc, CRplus_opp_r, CRplus_0_l, CRabs_opp.
-    rewrite CRplus_comm, <- CRplus_assoc, CRplus_opp_l.
-    rewrite CRplus_0_l. apply multiTriangleIneg.
-  - apply CR_cv_dist_cont. intros eps.
-    specialize (H eps) as [N lim].
-    exists N. intros. rewrite plus_comm. apply lim. apply (le_trans N i).
-    assumption. rewrite <- (plus_0_r i). rewrite <- plus_assoc.
-    apply Nat.add_le_mono_l. apply le_0_n.
-  - apply CR_cv_plus. 2: apply CR_cv_const. intros eps.
-    specialize (H0 eps) as [N lim].
-    exists N. intros. rewrite plus_comm. apply lim. apply (le_trans N i).
-    assumption. rewrite <- (plus_0_r i). rewrite <- plus_assoc.
-    apply Nat.add_le_mono_l. apply le_0_n.
-Qed.
-
-Lemma series_cv_minus : forall {R : ConstructiveReals}
-                          (u v : nat -> CRcarrier R) (s t : CRcarrier R),
-    series_cv u s
-    -> series_cv v t
-    -> series_cv (fun n => u n - v n) (s - t).
-Proof.
-  intros. apply (CR_cv_eq _ (fun n => CRsum u n - CRsum v n)).
-  intro n. symmetry. unfold CRminus. rewrite sum_plus.
-  rewrite sum_opp. reflexivity.
-  apply CR_cv_plus. exact H. apply CR_cv_opp. exact H0.
-Qed.
-
-Lemma series_cv_le : forall {R : ConstructiveReals}
-                       (un vn : nat -> CRcarrier R) (a b : CRcarrier R),
-    (forall n:nat, un n <= vn n)
-    -> series_cv un a
-    -> series_cv vn b
-    -> a <= b.
-Proof.
-  intros. apply (CRplus_le_reg_r (-a)). rewrite CRplus_opp_r.
-  apply (series_cv_nonneg (fun n => vn n - un n)).
-  intro n. apply (CRplus_le_reg_r (un n)).
-  rewrite CRplus_0_l. unfold CRminus.
-  rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r.
-  apply H. apply series_cv_minus; assumption.
-Qed.
-
-Lemma series_cv_series : forall {R : ConstructiveReals}
-                           (u : nat -> nat -> CRcarrier R) (s : nat -> CRcarrier R) (n : nat),
-    (forall i:nat, le i n -> series_cv (u i) (s i))
-    -> series_cv (fun i => CRsum (fun j => u j i) n) (CRsum s n).
-Proof.
-  induction n.
-  - intros. simpl. specialize (H O).
-    apply (series_cv_eq (u O)). reflexivity. apply H. apply le_refl.
-  - intros. simpl. apply (series_cv_plus). 2: apply (H (S n)).
-    apply IHn. 2: apply le_refl. intros. apply H.
-    apply (le_trans _ n _ H0). apply le_S. apply le_refl.
-Qed.
-
 Lemma CR_cv_shift :
   forall {R : ConstructiveReals} f k l,
     CR_cv R (fun n => f (n + k)%nat) l -> CR_cv R f l.
@@ -880,49 +478,3 @@ Proof.
   intros R f' k l cvf eps; destruct (cvf eps) as [N Pn].
   exists N; intros n nN; apply Pn; auto with arith.
 Qed.
-
-Lemma series_cv_shift :
-  forall {R : ConstructiveReals} (f : nat -> CRcarrier R) k l,
-    series_cv (fun n => f (S k + n)%nat) l
-    -> series_cv f (l + CRsum f k).
-Proof.
-  intros. intro p. specialize (H p) as [n nmaj].
-  exists (S k+n)%nat. intros. destruct (Nat.le_exists_sub (S k) i).
-  apply (le_trans _ (S k + 0)). rewrite Nat.add_0_r. apply le_refl.
-  apply (le_trans _ (S k + n)). apply Nat.add_le_mono_l, le_0_n.
-  exact H. destruct H0. subst i.
-  rewrite Nat.add_comm in H. rewrite <- Nat.add_le_mono_r in H.
-  specialize (nmaj x H). unfold CRminus.
-  rewrite Nat.add_comm, (sum_assoc f k x).
-  setoid_replace (CRsum f k + CRsum (fun k0 : nat => f (S k + k0)%nat) x - (l + CRsum f k))
-    with (CRsum (fun k0 : nat => f (S k + k0)%nat) x - l).
-  exact nmaj. unfold CRminus. rewrite (CRplus_comm (CRsum f k)).
-  rewrite CRplus_assoc. apply CRplus_morph. reflexivity.
-  rewrite CRplus_comm, CRopp_plus_distr, CRplus_assoc.
-  rewrite CRplus_opp_l, CRplus_0_r. reflexivity.
-Qed.
-
-Lemma series_cv_shift' : forall {R : ConstructiveReals}
-                           (un : nat -> CRcarrier R) (s : CRcarrier R) (shift : nat),
-    series_cv un s
-    -> series_cv (fun n => un (n+shift)%nat)
-                       (s - match shift with
-                            | O => 0
-                            | S p => CRsum un p
-                            end).
-Proof.
-  intros. destruct shift as [|p].
-  - unfold CRminus. rewrite CRopp_0. rewrite CRplus_0_r.
-    apply (series_cv_eq un). intros.
-    rewrite plus_0_r. reflexivity. apply H.
-  - apply (CR_cv_eq _ (fun n => CRsum un (n + S p) - CRsum un p)).
-    intros. rewrite plus_comm. unfold CRminus.
-    rewrite sum_assoc. simpl. rewrite CRplus_comm, <- CRplus_assoc.
-    rewrite CRplus_opp_l, CRplus_0_l.
-    apply CRsum_eq. intros. rewrite (plus_comm i). reflexivity.
-    apply CR_cv_plus. apply (CR_cv_shift' _ (S p) _ H).
-    intros n. exists (Pos.to_nat n). intros.
-    unfold CRminus. simpl.
-    rewrite CRopp_involutive, CRplus_opp_l. rewrite CRabs_right.
-    apply CR_of_Q_le. discriminate. apply CRle_refl.
-Qed.
diff --git a/theories/Reals/Abstract/ConstructiveMinMax.v b/theories/Reals/Abstract/ConstructiveMinMax.v
new file mode 100644
index 0000000000..b66d416ca4
--- /dev/null
+++ b/theories/Reals/Abstract/ConstructiveMinMax.v
@@ -0,0 +1,664 @@
+(************************************************************************)
+(*         *   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)         *)
+(************************************************************************)
+(************************************************************************)
+
+Require Import QArith.
+Require Import Qabs.
+Require Import ConstructiveReals.
+Require Import ConstructiveAbs.
+Require Import ConstructiveRealsMorphisms.
+
+Local Open Scope ConstructiveReals.
+
+(** Definition and properties of minimum and maximum.
+
+    WARNING: this file is experimental and likely to change in future releases.
+ *)
+
+
+(* Minimum *)
+
+Definition CRmin {R : ConstructiveReals} (x y : CRcarrier R) : CRcarrier R
+  := (x + y - CRabs _ (y - x)) * CR_of_Q _ (1#2).
+
+Lemma CRmin_lt_r : forall {R : ConstructiveReals} (x y : CRcarrier R),
+    CRmin x y < y -> CRmin x y == x.
+Proof.
+  intros. unfold CRmin. unfold CRmin in H.
+  apply (CRmult_eq_reg_r (CR_of_Q R 2)).
+  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 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.
+  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
+    with signature (CReq R) ==> (CReq R) ==> (CReq R)
+      as CRmin_morph.
+Proof.
+  intros. unfold CRmin.
+  apply CRmult_morph. 2: reflexivity.
+  unfold CRminus.
+  rewrite H, H0. reflexivity.
+Qed.
+
+Instance CRmin_morphT
+  : forall {R : ConstructiveReals},
+    CMorphisms.Proper
+      (CMorphisms.respectful (CReq R) (CMorphisms.respectful (CReq R) (CReq R))) (@CRmin R).
+Proof.
+  intros R x y H z t H0.
+  rewrite H, H0. reflexivity.
+Qed.
+
+Lemma CRmin_l : forall {R : ConstructiveReals} (x y : CRcarrier R),
+    CRmin x y <= x.
+Proof.
+  intros. unfold CRmin.
+  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 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))).
+  rewrite CRplus_opp_l, CRplus_0_l.
+  rewrite (CRplus_comm x), CRplus_assoc, CRplus_opp_l, CRplus_0_r.
+  apply CRle_abs.
+Qed.
+
+Lemma CRmin_r : forall {R : ConstructiveReals} (x y : CRcarrier R),
+    CRmin x y <= y.
+Proof.
+  intros. unfold CRmin.
+  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 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)).
+  rewrite <- CRplus_assoc, CRplus_opp_l, CRplus_0_l.
+  rewrite <- (CRopp_involutive y), <- CRopp_plus_distr, <- CRopp_plus_distr.
+  apply CRopp_ge_le_contravar. rewrite CRabs_opp, CRplus_comm.
+  apply CRle_abs.
+Qed.
+
+Lemma CRnegPartAbsMin : forall {R : ConstructiveReals} (x : CRcarrier R),
+    CRmin 0 x == (x - CRabs _ x) * (CR_of_Q _ (1#2)).
+Proof.
+  intros. unfold CRmin. unfold CRminus. rewrite CRplus_0_l.
+  apply CRmult_morph. 2: reflexivity. rewrite CRopp_0, CRplus_0_r. reflexivity.
+Qed.
+
+Lemma CRmin_sym : forall {R : ConstructiveReals} (x y : CRcarrier R),
+    CRmin x y == CRmin y x.
+Proof.
+  intros. unfold CRmin. apply CRmult_morph. 2: reflexivity.
+  rewrite CRabs_minus_sym. unfold CRminus.
+  rewrite (CRplus_comm x y). reflexivity.
+Qed.
+
+Lemma CRmin_mult :
+  forall {R : ConstructiveReals} (p q r : CRcarrier R),
+    0 <= r -> CRmin (r * p) (r * q) == r * CRmin p q.
+Proof.
+  intros R p q r H. unfold CRmin.
+  setoid_replace (r * q - r * p) with (r * (q - p)).
+  rewrite CRabs_mult.
+  rewrite (CRabs_right r). 2: exact H.
+  rewrite <- CRmult_assoc. apply CRmult_morph. 2: reflexivity.
+  unfold CRminus. rewrite CRopp_mult_distr_r.
+  do 2 rewrite <- CRmult_plus_distr_l. reflexivity.
+  unfold CRminus. rewrite CRopp_mult_distr_r.
+  rewrite <- CRmult_plus_distr_l. reflexivity.
+Qed.
+
+Lemma CRmin_plus : forall {R : ConstructiveReals} (x y z : CRcarrier R),
+    x + CRmin y z == CRmin (x + y) (x + z).
+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. 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 CRmult_1_r.
+  rewrite CRmult_assoc, <- CR_of_Q_mult.
+  setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity.
+  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.
+  rewrite CRopp_plus_distr. rewrite <- CRplus_assoc.
+  apply CRplus_morph. 2: reflexivity.
+  rewrite CRplus_comm, <- CRplus_assoc, CRplus_opp_l.
+  apply CRplus_0_l.
+Qed.
+
+Lemma CRmin_left : forall {R : ConstructiveReals} (x y : CRcarrier R),
+    x <= y -> CRmin x y == x.
+Proof.
+  intros. unfold CRmin.
+  apply (CRmult_eq_reg_r (CR_of_Q R 2)).
+  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 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.
+  rewrite <- (CRplus_opp_r x). apply CRplus_le_compat.
+  exact H. apply CRle_refl.
+Qed.
+
+Lemma CRmin_right : forall {R : ConstructiveReals} (x y : CRcarrier R),
+    y <= x -> CRmin x y == y.
+Proof.
+  intros. unfold CRmin.
+  apply (CRmult_eq_reg_r (CR_of_Q R 2)).
+  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 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.
+  do 2 rewrite CRopp_involutive.
+  rewrite CRplus_comm, CRplus_assoc, CRplus_opp_l, CRplus_0_r. reflexivity.
+  rewrite <- (CRplus_opp_r x). apply CRplus_le_compat.
+  exact H. apply CRle_refl.
+Qed.
+
+Lemma CRmin_lt : forall {R : ConstructiveReals} (x y z : CRcarrier R),
+    z < x -> z < y -> z < CRmin x y.
+Proof.
+  intros. unfold CRmin.
+  apply (CRmult_lt_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 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))).
+  rewrite (CRplus_comm (x+y)), CRplus_assoc.
+  rewrite <- (CRplus_assoc (CRabs R (y + - x))), CRplus_opp_r, CRplus_0_l.
+  rewrite <- (CRplus_comm (x+y)).
+  apply CRabs_def1.
+  - unfold CRminus. rewrite <- (CRplus_comm y), CRplus_assoc.
+    apply CRplus_lt_compat_l.
+    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), CRmult_plus_distr_l.
+    rewrite CRmult_1_r. apply CRplus_le_lt_compat.
+    apply CRlt_asym.
+    apply CRopp_gt_lt_contravar, H.
+    apply CRopp_gt_lt_contravar, H.
+  - rewrite CRopp_plus_distr, CRopp_involutive.
+    rewrite CRplus_comm, CRplus_assoc.
+    apply CRplus_lt_compat_l.
+    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), CRmult_plus_distr_l.
+    rewrite CRmult_1_r. apply CRplus_le_lt_compat.
+    apply CRlt_asym.
+    apply CRopp_gt_lt_contravar, H0.
+    apply CRopp_gt_lt_contravar, H0.
+Qed.
+
+Lemma CRmin_contract : forall {R : ConstructiveReals} (x y a : CRcarrier R),
+    CRabs _ (CRmin x a - CRmin y a) <= CRabs _ (x - y).
+Proof.
+  intros. unfold CRmin.
+  unfold CRminus. rewrite CRopp_mult_distr_l, <- CRmult_plus_distr_r.
+  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: 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.
+  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.
+  rewrite (CRabs_morph (x-y) ((a-y)-(a-x))).
+  apply CRabs_triang_inv2.
+  unfold CRminus. rewrite (CRplus_comm (a + - y)).
+  rewrite <- CRplus_assoc. apply CRplus_morph. 2: reflexivity.
+  rewrite CRplus_comm, CRopp_plus_distr, <- CRplus_assoc.
+  rewrite CRplus_opp_r, CRopp_involutive, CRplus_0_l.
+  reflexivity.
+  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 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.
+  rewrite CRplus_assoc. apply CRplus_morph. reflexivity.
+  rewrite CRopp_plus_distr. rewrite (CRplus_comm (-a)).
+  rewrite CRplus_assoc, <- (CRplus_assoc (-a)), CRplus_opp_l.
+  rewrite CRplus_0_l, CRopp_involutive. reflexivity.
+Qed.
+
+Lemma CRmin_glb : forall {R : ConstructiveReals} (x y z:CRcarrier R),
+    z <= x -> z <= y -> z <= CRmin x y.
+Proof.
+  intros. unfold CRmin.
+  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 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))).
+  rewrite CRplus_assoc, <- (CRplus_assoc (- CRabs R (y + - x))).
+  rewrite CRplus_opp_l, CRplus_0_l.
+  apply CRabs_le. split.
+  - do 2 rewrite CRopp_plus_distr.
+    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), 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), CRmult_plus_distr_l.
+    rewrite CRmult_1_r.
+    apply CRplus_le_compat; apply CRopp_ge_le_contravar; exact H.
+Qed.
+
+Lemma CRmin_assoc : forall {R : ConstructiveReals} (a b c : CRcarrier R),
+    CRmin a (CRmin b c) == CRmin (CRmin a b) c.
+Proof.
+  split.
+  - apply CRmin_glb.
+    + apply (CRle_trans _ (CRmin a b)).
+      apply CRmin_l. apply CRmin_l.
+    + apply CRmin_glb.
+      apply (CRle_trans _ (CRmin a b)).
+      apply CRmin_l. apply CRmin_r. apply CRmin_r.
+  - apply CRmin_glb.
+    + apply CRmin_glb. apply CRmin_l.
+      apply (CRle_trans _ (CRmin b c)).
+      apply CRmin_r. apply CRmin_l.
+    + apply (CRle_trans _ (CRmin b c)).
+      apply CRmin_r. apply CRmin_r.
+Qed.
+
+Lemma CRlt_min : forall {R : ConstructiveReals} (x y z : CRcarrier R),
+    z < CRmin x y -> prod (z < x) (z < y).
+Proof.
+  intros. destruct (CR_Q_dense R _ _ H) as [q qmaj].
+  destruct qmaj.
+  split.
+  - apply (CRlt_le_trans _ (CR_of_Q R q) _ c).
+    intro abs. apply (CRlt_asym _ _ c0).
+    apply (CRle_lt_trans _ x). apply CRmin_l. exact abs.
+  - apply (CRlt_le_trans _ (CR_of_Q R q) _ c).
+    intro abs. apply (CRlt_asym _ _ c0).
+    apply (CRle_lt_trans _ y). apply CRmin_r. exact abs.
+Qed.
+
+
+
+(* Maximum *)
+
+Definition CRmax {R : ConstructiveReals} (x y : CRcarrier R) : CRcarrier R
+  := (x + y + CRabs _ (y - x)) * CR_of_Q _ (1#2).
+
+Add Parametric Morphism {R : ConstructiveReals} : CRmax
+    with signature (CReq R) ==> (CReq R) ==> (CReq R)
+      as CRmax_morph.
+Proof.
+  intros. unfold CRmax.
+  apply CRmult_morph. 2: reflexivity. unfold CRminus.
+  rewrite H, H0. reflexivity.
+Qed.
+
+Instance CRmax_morphT
+  : forall {R : ConstructiveReals},
+    CMorphisms.Proper
+      (CMorphisms.respectful (CReq R) (CMorphisms.respectful (CReq R) (CReq R))) (@CRmax R).
+Proof.
+  intros R x y H z t H0.
+  rewrite H, H0. reflexivity.
+Qed.
+
+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)).
+  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 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.
+  apply CRabs_le. split.
+  - repeat rewrite CRopp_plus_distr.
+    do 2 rewrite CRopp_involutive.
+    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, 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, CRmult_1_r.
+    apply CRplus_le_compat; assumption.
+Qed.
+
+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)).
+  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 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)).
+  rewrite <- CRplus_assoc, CRplus_opp_l, CRplus_0_l.
+  rewrite CRabs_minus_sym, CRplus_comm.
+  apply CRle_abs. reflexivity.
+Qed.
+
+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)).
+  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 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)).
+  rewrite <- CRplus_assoc, CRplus_opp_l, CRplus_0_l.
+  rewrite CRplus_comm. apply CRle_abs.
+Qed.
+
+Lemma CRposPartAbsMax : forall {R : ConstructiveReals} (x : CRcarrier R),
+    CRmax 0 x == (x + CRabs _ x) * (CR_of_Q R (1#2)).
+Proof.
+  intros. unfold CRmax. unfold CRminus. rewrite CRplus_0_l.
+  apply CRmult_morph. 2: reflexivity. rewrite CRopp_0, CRplus_0_r. reflexivity.
+Qed.
+
+Lemma CRmax_sym : forall {R : ConstructiveReals} (x y : CRcarrier R),
+    CRmax x y == CRmax y x.
+Proof.
+  intros. unfold CRmax.
+  rewrite CRabs_minus_sym. apply CRmult_morph.
+  2: reflexivity. rewrite (CRplus_comm x y). reflexivity.
+Qed.
+
+Lemma CRmax_plus : forall {R : ConstructiveReals} (x y z : CRcarrier R),
+    x + CRmax y z == CRmax (x + y) (x + z).
+Proof.
+  intros. unfold CRmax.
+  setoid_replace (x + z - (x + y)) with (z-y).
+  apply (CRmult_eq_reg_r (CR_of_Q _ 2)).
+  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 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, 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.
+  rewrite (CRplus_comm x). apply CRplus_assoc.
+  unfold CRminus. rewrite CRopp_plus_distr. rewrite <- CRplus_assoc.
+  apply CRplus_morph. 2: reflexivity.
+  rewrite CRplus_comm, <- CRplus_assoc, CRplus_opp_l.
+  apply CRplus_0_l.
+Qed.
+
+Lemma CRmax_left : forall {R : ConstructiveReals} (x y : CRcarrier R),
+    y <= x -> CRmax x y == x.
+Proof.
+  intros. unfold CRmax.
+  apply (CRmult_eq_reg_r (CR_of_Q R 2)).
+  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 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.
+  rewrite <- (CRplus_opp_r x). apply CRplus_le_compat_r. exact H.
+Qed.
+
+Lemma CRmax_right : forall {R : ConstructiveReals} (x y : CRcarrier R),
+    x <= y -> CRmax x y == y.
+Proof.
+  intros. unfold CRmax.
+  apply (CRmult_eq_reg_r (CR_of_Q R 2)).
+  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 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.
+  rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r. reflexivity.
+  rewrite <- (CRplus_opp_r x). apply CRplus_le_compat_r. exact H.
+Qed.
+
+Lemma CRmax_contract : forall {R : ConstructiveReals} (x y a : CRcarrier R),
+    CRabs _ (CRmax x a - CRmax y a) <= CRabs _ (x - y).
+Proof.
+  intros. unfold CRmax.
+  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: 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.
+  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.
+  rewrite (CRabs_minus_sym x y).
+  rewrite (CRabs_morph (y-x) ((a-x)-(a-y))).
+  apply CRabs_triang_inv2.
+  unfold CRminus. rewrite (CRplus_comm (a + - x)).
+  rewrite <- CRplus_assoc. apply CRplus_morph. 2: reflexivity.
+  rewrite CRplus_comm, CRopp_plus_distr, <- CRplus_assoc.
+  rewrite CRplus_opp_r, CRopp_involutive, CRplus_0_l.
+  reflexivity.
+  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 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.
+  rewrite <- CRplus_assoc. rewrite CRplus_comm, CRopp_plus_distr.
+  rewrite CRplus_assoc. apply CRplus_morph. reflexivity.
+  rewrite CRopp_plus_distr. rewrite (CRplus_comm (-a)).
+  rewrite CRplus_assoc, <- (CRplus_assoc (-a)), CRplus_opp_l.
+  rewrite CRplus_0_l. apply CRplus_comm.
+Qed.
+
+Lemma CRmax_lub_lt : forall {R : ConstructiveReals} (x y z : CRcarrier R),
+    x < z -> y < z -> CRmax x y < z.
+Proof.
+  intros. unfold CRmax.
+  apply (CRmult_lt_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 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.
+  apply CRabs_def1.
+  - rewrite (CRplus_comm y), (CRplus_comm (-y)), CRplus_assoc.
+    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), 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), CRmult_plus_distr_l.
+    rewrite CRmult_1_r. apply CRplus_le_lt_compat.
+    apply CRlt_asym, H. exact H.
+Qed.
+
+Lemma CRmax_assoc : forall {R : ConstructiveReals} (a b c : CRcarrier R),
+    CRmax a (CRmax b c) == CRmax (CRmax a b) c.
+Proof.
+  split.
+  - apply CRmax_lub.
+    + apply CRmax_lub. apply CRmax_l.
+      apply (CRle_trans _ (CRmax b c)).
+      apply CRmax_l. apply CRmax_r.
+    + apply (CRle_trans _ (CRmax b c)).
+      apply CRmax_r. apply CRmax_r.
+  - apply CRmax_lub.
+    + apply (CRle_trans _ (CRmax a b)).
+      apply CRmax_l. apply CRmax_l.
+    + apply CRmax_lub.
+      apply (CRle_trans _ (CRmax a b)).
+      apply CRmax_r. apply CRmax_l. apply CRmax_r.
+Qed.
+
+Lemma CRmax_min_mult_neg :
+  forall {R : ConstructiveReals} (p q r:CRcarrier R),
+    r <= 0 -> CRmax (r * p) (r * q) == r * CRmin p q.
+Proof.
+  intros R p q r H. unfold CRmin, CRmax.
+  setoid_replace (r * q - r * p) with (r * (q - p)).
+  rewrite CRabs_mult.
+  rewrite (CRabs_left r), <- CRmult_assoc.
+  apply CRmult_morph. 2: reflexivity. unfold CRminus.
+  rewrite <- CRopp_mult_distr_l, CRopp_mult_distr_r,
+  CRmult_plus_distr_l, CRmult_plus_distr_l.
+  reflexivity. exact H.
+  unfold CRminus. rewrite CRmult_plus_distr_l, CRopp_mult_distr_r. reflexivity.
+Qed.
+
+Lemma CRlt_max : forall {R : ConstructiveReals} (x y z : CRcarrier R),
+    CRmax x y < z -> prod (x < z) (y < z).
+Proof.
+  intros. destruct (CR_Q_dense R _ _ H) as [q qmaj].
+  destruct qmaj.
+  split.
+  - apply (CRlt_le_trans _ (CR_of_Q R q)).
+    apply (CRle_lt_trans _ (CRmax x y)). apply CRmax_l. exact c.
+    apply CRlt_asym, c0.
+  - apply (CRlt_le_trans _ (CR_of_Q R q)).
+    apply (CRle_lt_trans _ (CRmax x y)). apply CRmax_r. exact c.
+    apply CRlt_asym, c0.
+Qed.
+
+Lemma CRmax_mult :
+  forall {R : ConstructiveReals} (p q r:CRcarrier R),
+    0 <= r -> CRmax (r * p) (r * q) == r * CRmax p q.
+Proof.
+  intros R p q r H. unfold CRmin, CRmax.
+  setoid_replace (r * q - r * p) with (r * (q - p)).
+  rewrite CRabs_mult.
+  rewrite (CRabs_right r), <- CRmult_assoc.
+  apply CRmult_morph. 2: reflexivity.
+  rewrite CRmult_plus_distr_l, CRmult_plus_distr_l.
+  reflexivity. exact H.
+  unfold CRminus. rewrite CRmult_plus_distr_l, CRopp_mult_distr_r. reflexivity.
+Qed.
+
+Lemma CRmin_max_mult_neg :
+  forall {R : ConstructiveReals} (p q r:CRcarrier R),
+    r <= 0 -> CRmin (r * p) (r * q) == r * CRmax p q.
+Proof.
+  intros R p q r H. unfold CRmin, CRmax.
+  setoid_replace (r * q - r * p) with (r * (q - p)).
+  rewrite CRabs_mult.
+  rewrite (CRabs_left r), <- CRmult_assoc.
+  apply CRmult_morph. 2: reflexivity. unfold CRminus.
+  rewrite CRopp_mult_distr_l, CRopp_involutive,
+  CRmult_plus_distr_l, CRmult_plus_distr_l.
+  reflexivity. exact H.
+  unfold CRminus. rewrite CRmult_plus_distr_l, CRopp_mult_distr_r. reflexivity.
+Qed.
+
+Lemma CRmorph_min : forall {R1 R2 : ConstructiveReals}
+                      (f : @ConstructiveRealsMorphism R1 R2)
+                      (a b : CRcarrier R1),
+    CRmorph f (CRmin a b)
+    == CRmin (CRmorph f a) (CRmorph f b).
+Proof.
+  intros. unfold CRmin.
+  rewrite CRmorph_mult. apply CRmult_morph.
+  2: apply CRmorph_rat.
+  unfold CRminus. do 2 rewrite CRmorph_plus. apply CRplus_morph.
+  apply CRplus_morph. reflexivity. reflexivity.
+  rewrite CRmorph_opp. apply CRopp_morph.
+  rewrite <- CRmorph_abs. apply CRabs_morph.
+  rewrite CRmorph_plus. apply CRplus_morph.
+  reflexivity.
+  rewrite CRmorph_opp. apply CRopp_morph, CRmorph_proper. reflexivity.
+Qed.
diff --git a/theories/Reals/Abstract/ConstructivePower.v b/theories/Reals/Abstract/ConstructivePower.v
new file mode 100644
index 0000000000..2bde1aef42
--- /dev/null
+++ b/theories/Reals/Abstract/ConstructivePower.v
@@ -0,0 +1,251 @@
+(************************************************************************)
+(*         *   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)         *)
+(************************************************************************)
+
+Require Import QArith Qabs.
+Require Import ConstructiveReals.
+Require Import ConstructiveRealsMorphisms.
+Require Import ConstructiveAbs.
+Require Import ConstructiveLimits.
+Require Import ConstructiveSum.
+
+Local Open Scope ConstructiveReals.
+
+
+(**
+   Definition and properties of powers.
+
+   WARNING: this file is experimental and likely to change in future releases.
+*)
+
+Fixpoint CRpow {R : ConstructiveReals} (r:CRcarrier R) (n:nat) : CRcarrier R :=
+  match n with
+    | O => 1
+    | S n => r * (CRpow r n)
+  end.
+
+Lemma CRpow_ge_one : forall {R : ConstructiveReals} (x : CRcarrier R) (n : nat),
+    1 <= x
+    -> 1 <= CRpow x n.
+Proof.
+  induction n.
+  - intros. apply CRle_refl.
+  - intros. simpl. apply (CRle_trans _ (x * 1)).
+    rewrite CRmult_1_r. exact H.
+    apply CRmult_le_compat_l_half. apply (CRlt_le_trans _ 1).
+    apply CRzero_lt_one. exact H.
+    apply IHn. exact H.
+Qed.
+
+Lemma CRpow_ge_zero : forall {R : ConstructiveReals} (x : CRcarrier R) (n : nat),
+    0 <= x
+    -> 0 <= CRpow x n.
+Proof.
+  induction n.
+  - intros. apply CRlt_asym, CRzero_lt_one.
+  - intros. simpl. apply CRmult_le_0_compat.
+    exact H. apply IHn. exact H.
+Qed.
+
+Lemma CRpow_gt_zero : forall {R : ConstructiveReals} (x : CRcarrier R) (n : nat),
+    0 < x
+    -> 0 < CRpow x n.
+Proof.
+  induction n.
+  - intros. apply CRzero_lt_one.
+  - intros. simpl. apply CRmult_lt_0_compat. exact H.
+    apply IHn. exact H.
+Qed.
+
+Lemma CRpow_mult : forall {R : ConstructiveReals} (x y : CRcarrier R) (n:nat),
+    CRpow x n * CRpow y n == CRpow (x*y) n.
+Proof.
+  induction n.
+  - simpl. rewrite CRmult_1_r. reflexivity.
+  - simpl. rewrite <- IHn. do 2 rewrite <- (Rmul_assoc (CRisRing R)).
+    apply CRmult_morph. reflexivity.
+    rewrite <- (Rmul_comm (CRisRing R)). rewrite <- (Rmul_assoc (CRisRing R)).
+    apply CRmult_morph. reflexivity.
+    rewrite <- (Rmul_comm (CRisRing R)). reflexivity.
+Qed.
+
+Lemma CRpow_one : forall {R : ConstructiveReals} (n:nat),
+    @CRpow R 1 n == 1.
+Proof.
+  induction n. reflexivity.
+  transitivity (CRmult R 1 (CRpow 1 n)). reflexivity.
+  rewrite IHn. rewrite CRmult_1_r. reflexivity.
+Qed.
+
+Lemma CRpow_proper : forall {R : ConstructiveReals} (x y : CRcarrier R) (n : nat),
+    x == y -> CRpow x n == CRpow y n.
+Proof.
+  induction n.
+  - intros. reflexivity.
+  - intros. simpl. rewrite IHn, H. reflexivity. exact H.
+Qed.
+
+Lemma CRpow_inv : forall {R : ConstructiveReals} (x : CRcarrier R) (xPos : 0 < x) (n : nat),
+    CRpow (CRinv R x (inr xPos)) n
+    == CRinv R (CRpow x n) (inr (CRpow_gt_zero x n xPos)).
+Proof.
+  induction n.
+  - rewrite CRinv_1. reflexivity.
+  - transitivity (CRinv R x (inr xPos) * CRpow (CRinv R x (inr xPos)) n).
+    reflexivity. rewrite IHn.
+    assert (0 < x * CRpow x n).
+    { apply CRmult_lt_0_compat. exact xPos. apply CRpow_gt_zero, xPos. }
+    rewrite <- (CRinv_mult_distr _ _ _ _ (inr H)).
+    apply CRinv_morph. reflexivity.
+Qed.
+
+Lemma CRpow_plus_distr : forall {R : ConstructiveReals} (x : CRcarrier R) (n p:nat),
+    CRpow x n * CRpow x p == CRpow x (n+p).
+Proof.
+  induction n.
+  - intros. simpl. rewrite CRmult_1_l. reflexivity.
+  - intros. simpl. rewrite CRmult_assoc. apply CRmult_morph.
+    reflexivity. apply IHn.
+Qed.
+
+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.
+  rewrite CRmult_plus_distr_r, CRmult_1_l. reflexivity.
+Qed.
+
+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.
+    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))).
+    2: symmetry; apply Qinv_plus_distr.
+    rewrite CR_of_Q_plus.
+    replace (CRpow (CR_of_Q R 2) (1 + n))
+      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.
+    apply CRpow_ge_one. 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 CRpow_ge_zero; apply CR_of_Q_le; discriminate.
+  apply CRlt_asym.
+  apply (CRmult_lt_reg_l (CR_of_Q R (Z.pos p # 1))).
+  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 CRpow_gt_zero.
+  apply CR_of_Q_lt. reflexivity.
+  rewrite CRmult_assoc. rewrite CRpow_mult.
+  rewrite (CRpow_proper (CR_of_Q R (1 # 2) * CR_of_Q R 2) 1), CRpow_one.
+  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.
+  reflexivity. reflexivity.
+Qed.
+
+Lemma GeoFiniteSum : forall {R : ConstructiveReals} (n:nat),
+    CRsum (CRpow (CR_of_Q R (1#2))) n == CR_of_Q R 2 - CRpow (CR_of_Q R (1#2)) n.
+Proof.
+  induction n.
+  - unfold CRsum, CRpow. simpl (1%ConstructiveReals).
+    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.
+    rewrite IHn. clear IHn. unfold CRminus.
+    rewrite CRplus_assoc. apply CRplus_morph. reflexivity.
+    apply (CRplus_eq_reg_l
+             (CRpow (CR_of_Q R (1 # 2)) n + CRpow (CR_of_Q R (1 # 2)) (S n))).
+    rewrite (CRplus_assoc _ _ (-CRpow (CR_of_Q R (1 # 2)) (S n))),
+    CRplus_opp_r, CRplus_0_r.
+    rewrite (CRplus_comm (CRpow (CR_of_Q R (1 # 2)) n)), CRplus_assoc.
+    rewrite <- (CRplus_assoc (CRpow (CR_of_Q R (1 # 2)) n)), CRplus_opp_r,
+    CRplus_0_l, <- CR_double.
+    setoid_replace (CRpow (CR_of_Q R (1 # 2)) (S n))
+      with (CR_of_Q R (1 # 2) * CRpow (CR_of_Q R (1 # 2)) n).
+    2: reflexivity.
+    rewrite <- CRmult_assoc, <- CR_of_Q_mult.
+    setoid_replace (2 * (1 # 2))%Q with 1%Q.
+    apply CRmult_1_l. reflexivity.
+Qed.
+
+Lemma GeoHalfBelowTwo : forall {R : ConstructiveReals} (n:nat),
+    CRsum (CRpow (CR_of_Q R (1#2))) n < CR_of_Q R 2.
+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 CRpow_gt_zero. apply CR_of_Q_lt. reflexivity.
+Qed.
+
+Lemma GeoHalfTwo : forall {R : ConstructiveReals},
+    series_cv (fun n => CRpow (CR_of_Q R (1#2)) n) (CR_of_Q R 2).
+Proof.
+  intro R.
+  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.
+      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.
+      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 CRpow_ge_one. 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).
+    { apply CR_of_Q_lt. reflexivity. }
+    rewrite (CRpow_proper _ (CRinv R (CR_of_Q R 2) (inr H1))).
+    rewrite CRpow_inv. apply CRlt_asym.
+    apply (CRmult_lt_reg_l (CRpow (CR_of_Q R 2) i)). apply CRpow_gt_zero, H1.
+    rewrite CRinv_r.
+    apply (CRmult_lt_reg_r (CR_of_Q R (Z.pos n#1))).
+    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 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).
+    rewrite H3 in H2. inversion H2.
+    apply Pos2Z.pos_le_pos. apply Pos2Nat.inj_le.
+    apply (le_trans _ _ _ H0). rewrite SuccNat2Pos.id_succ. apply le_refl.
+    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.
+    reflexivity. reflexivity.
+    apply CRlt_asym, CRpow_gt_zero.
+    apply CR_of_Q_lt. reflexivity.
+    unfold CRminus. rewrite CRplus_comm, <- CRplus_assoc.
+    rewrite CRplus_opp_l, CRplus_0_l. reflexivity.
+Qed.
diff --git a/theories/Reals/Abstract/ConstructiveReals.v b/theories/Reals/Abstract/ConstructiveReals.v
index 019428a5b0..60fad8795a 100644
--- a/theories/Reals/Abstract/ConstructiveReals.v
+++ b/theories/Reals/Abstract/ConstructiveReals.v
@@ -64,7 +64,10 @@ Structure R := {
   on the real numbers. In "Sheaves in Geometry and Logic",
   MacLane and Moerdijk show a topos in which all functions R -> Z
   are constant. Consequently all functions R -> Q are constant and
-  it is not possible to approximate real numbers by rational numbers. *)
+  it is not possible to approximate real numbers by rational numbers.
+
+  WARNING: this file is experimental and likely to change in future releases.
+ *)
 
 
 Require Import QArith Qabs Qround.
diff --git a/theories/Reals/Abstract/ConstructiveRealsMorphisms.v b/theories/Reals/Abstract/ConstructiveRealsMorphisms.v
index cf302dc847..53b5aca38c 100644
--- a/theories/Reals/Abstract/ConstructiveRealsMorphisms.v
+++ b/theories/Reals/Abstract/ConstructiveRealsMorphisms.v
@@ -23,14 +23,16 @@
 
     Apart from the speed, those unique isomorphisms also serve as
     sanity checks of the interface ConstructiveReals :
-    it captures a concept with a strong notion of uniqueness. *)
+    it captures a concept with a strong notion of uniqueness.
+
+    WARNING: this file is experimental and likely to change in future releases.
+*)
 
 Require Import QArith.
 Require Import Qabs.
 Require Import ConstructiveReals.
 Require Import ConstructiveLimits.
 Require Import ConstructiveAbs.
-Require Import ConstructiveSum.
 
 Local Open Scope ConstructiveReals.
 
@@ -889,37 +891,6 @@ Proof.
   apply CRmorph_one.
 Qed.
 
-Lemma CRmorph_sum : forall {R1 R2 : ConstructiveReals}
-                      (f : @ConstructiveRealsMorphism R1 R2)
-                      (un : nat -> CRcarrier R1) (n : nat),
-  CRmorph f (CRsum un n) ==
-  CRsum (fun n0 : nat => CRmorph f (un n0)) n.
-Proof.
-  induction n.
-  - reflexivity.
-  - simpl. rewrite CRmorph_plus, IHn. reflexivity.
-Qed.
-
-Lemma CRmorph_INR : forall {R1 R2 : ConstructiveReals}
-                      (f : @ConstructiveRealsMorphism R1 R2)
-                      (n : nat),
-  CRmorph f (INR n) == INR n.
-Proof.
-  induction n.
-  - apply CRmorph_rat.
-  - 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_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_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.
-Qed.
-
 Lemma CRmorph_rat_cv
   : forall {R1 R2 : ConstructiveReals}
            (qn : nat -> Q),
@@ -1139,34 +1110,3 @@ Proof.
   rewrite <- (CRmorph_rat f (1#p)) in H.
   apply (CRmorph_le_inv f) in H. exact H.
 Qed.
-
-Lemma CRmorph_min : forall {R1 R2 : ConstructiveReals}
-                      (f : @ConstructiveRealsMorphism R1 R2)
-                      (a b : CRcarrier R1),
-    CRmorph f (CRmin a b)
-    == CRmin (CRmorph f a) (CRmorph f b).
-Proof.
-  intros. unfold CRmin.
-  rewrite CRmorph_mult. apply CRmult_morph.
-  2: apply CRmorph_rat.
-  unfold CRminus. do 2 rewrite CRmorph_plus. apply CRplus_morph.
-  apply CRplus_morph. reflexivity. reflexivity.
-  rewrite CRmorph_opp. apply CRopp_morph.
-  rewrite <- CRmorph_abs. apply CRabs_morph.
-  rewrite CRmorph_plus. apply CRplus_morph.
-  reflexivity.
-  rewrite CRmorph_opp. apply CRopp_morph, CRmorph_proper. reflexivity.
-Qed.
-
-Lemma CRmorph_series_cv : forall {R1 R2 : ConstructiveReals}
-                     (f : @ConstructiveRealsMorphism R1 R2)
-                     (un : nat -> CRcarrier R1)
-                     (l : CRcarrier R1),
-    series_cv un l
-    -> series_cv (fun n => CRmorph f (un n)) (CRmorph f l).
-Proof.
-  intros.
-  apply (CR_cv_eq _ (fun n => CRmorph f (CRsum un n))).
-  intro n. apply CRmorph_sum.
-  apply CRmorph_cv, H.
-Qed.
diff --git a/theories/Reals/Abstract/ConstructiveSum.v b/theories/Reals/Abstract/ConstructiveSum.v
index 3be03bf615..147c45e4f4 100644
--- a/theories/Reals/Abstract/ConstructiveSum.v
+++ b/theories/Reals/Abstract/ConstructiveSum.v
@@ -10,13 +10,17 @@
 
 Require Import QArith Qabs.
 Require Import ConstructiveReals.
+Require Import ConstructiveRealsMorphisms.
 Require Import ConstructiveAbs.
+Require Import ConstructiveLimits.
 
 Local Open Scope ConstructiveReals.
 
 
 (**
    Definition and properties of finite sums and powers.
+
+   WARNING: this file is experimental and likely to change in future releases.
 *)
 
 Fixpoint CRsum {R : ConstructiveReals}
@@ -26,12 +30,6 @@ Fixpoint CRsum {R : ConstructiveReals}
     | S i => CRsum f i + f (S i)
   end.
 
-Fixpoint CRpow {R : ConstructiveReals} (r:CRcarrier R) (n:nat) : CRcarrier R :=
-  match n with
-    | O => 1
-    | S n => r * (CRpow r n)
-  end.
-
 Lemma CRsum_eq :
   forall {R : ConstructiveReals} (An Bn:nat -> CRcarrier R) (N:nat),
     (forall i:nat, (i <= N)%nat -> An i == Bn i) ->
@@ -260,89 +258,333 @@ Proof.
     reflexivity. rewrite CRplus_0_r. rewrite CRplus_assoc. reflexivity.
 Qed.
 
+Definition series_cv {R : ConstructiveReals}
+           (un : nat -> CRcarrier R) (s : CRcarrier R) : Set
+  := CR_cv R (CRsum un) s.
+
+Definition series_cv_lim_lt {R : ConstructiveReals}
+           (un : nat -> CRcarrier R) (x : CRcarrier R) : Set
+  := { l : CRcarrier R & prod (series_cv un l) (l < x) }.
 
-(* Power *)
+Definition series_cv_le_lim {R : ConstructiveReals}
+           (x : CRcarrier R) (un : nat -> CRcarrier R) : Set
+  := { l : CRcarrier R & prod (series_cv un l) (x <= l) }.
 
-Lemma pow_R1_Rle : forall {R : ConstructiveReals} (x : CRcarrier R) (n : nat),
-    1 <= x
-    -> 1 <= CRpow x n.
+Lemma series_cv_maj : forall {R : ConstructiveReals}
+                        (un vn : nat -> CRcarrier R) (s : CRcarrier R),
+    (forall n:nat, CRabs R (un n) <= vn n)
+    -> series_cv vn s
+    -> { l : CRcarrier R & prod (series_cv un l) (l <= s) }.
 Proof.
-  induction n.
-  - intros. apply CRle_refl.
-  - intros. simpl. apply (CRle_trans _ (x * 1)).
-    rewrite CRmult_1_r. exact H.
-    apply CRmult_le_compat_l_half. apply (CRlt_le_trans _ 1).
-    apply CRzero_lt_one. exact H.
-    apply IHn. exact H.
+  intros. destruct (CR_complete R (CRsum un)).
+  - intros n.
+    specialize (H0 (2*n)%positive) as [N maj].
+    exists N. intros i j H0 H1.
+    apply (CRle_trans _ (CRsum vn (max i j) - CRsum vn (min i j))).
+    apply Abs_sum_maj. apply H.
+    setoid_replace (CRsum vn (max i j) - CRsum vn (min i j))
+      with (CRabs R (CRsum vn (max i j) - (CRsum vn (min i j)))).
+    setoid_replace (CRsum vn (Init.Nat.max i j) - CRsum vn (Init.Nat.min i j))
+      with (CRsum vn (Init.Nat.max i j) - s - (CRsum vn (Init.Nat.min i j) - s)).
+    apply (CRle_trans _ _ _ (CRabs_triang _ _)).
+    setoid_replace (1#n)%Q with ((1#2*n) + (1#2*n))%Q.
+    rewrite CR_of_Q_plus.
+    apply CRplus_le_compat.
+    apply maj. apply (le_trans _ i). assumption. apply Nat.le_max_l.
+    rewrite CRabs_opp. apply maj.
+    apply Nat.min_case. apply (le_trans _ i). assumption. apply le_refl.
+    assumption. rewrite Qinv_plus_distr. reflexivity.
+    unfold CRminus. rewrite CRplus_assoc. apply CRplus_morph.
+    reflexivity. rewrite CRopp_plus_distr, CRopp_involutive.
+    rewrite CRplus_comm, CRplus_assoc, CRplus_opp_r, CRplus_0_r.
+    reflexivity.
+    rewrite CRabs_right. reflexivity.
+    rewrite <- (CRplus_opp_r (CRsum vn (Init.Nat.min i j))).
+    apply CRplus_le_compat. apply pos_sum_more.
+    intros. apply (CRle_trans _ (CRabs R (un k))). apply CRabs_pos.
+    apply H. apply (le_trans _ i). apply Nat.le_min_l. apply Nat.le_max_l.
+    apply CRle_refl.
+  - exists x. split. assumption.
+    (* x <= s *)
+    apply (CRplus_le_reg_r (-x)). rewrite CRplus_opp_r.
+    apply (CR_cv_bound_down (fun n => CRsum vn n - CRsum un n) _ _ 0).
+    intros. rewrite <- (CRplus_opp_r (CRsum un n)).
+    apply CRplus_le_compat. apply sum_Rle.
+    intros. apply (CRle_trans _ (CRabs R (un k))).
+    apply CRle_abs. apply H. apply CRle_refl.
+    apply CR_cv_plus. assumption.
+    apply CR_cv_opp. assumption.
 Qed.
 
-Lemma pow_le : forall {R : ConstructiveReals} (x : CRcarrier R) (n : nat),
-    0 <= x
-    -> 0 <= CRpow x n.
+Lemma series_cv_abs_lt
+  : forall {R : ConstructiveReals} (un vn : nat -> CRcarrier R) (l : CRcarrier R),
+    (forall n:nat, CRabs R (un n) <= vn n)
+    -> series_cv_lim_lt vn l
+    -> series_cv_lim_lt un l.
 Proof.
-  induction n.
-  - intros. apply CRlt_asym, CRzero_lt_one.
-  - intros. simpl. apply CRmult_le_0_compat.
-    exact H. apply IHn. exact H.
+  intros. destruct H0 as [x [H0 H1]].
+  destruct (series_cv_maj un vn x H H0) as [x0 H2].
+  exists x0. split. apply H2. apply (CRle_lt_trans _ x).
+  apply H2. apply H1.
 Qed.
 
-Lemma pow_lt : forall {R : ConstructiveReals} (x : CRcarrier R) (n : nat),
-    0 < x
-    -> 0 < CRpow x n.
+Definition series_cv_abs {R : ConstructiveReals} (u : nat -> CRcarrier R)
+  : CR_cauchy R (CRsum (fun n => CRabs R (u n)))
+    -> { l : CRcarrier R & series_cv u l }.
 Proof.
-  induction n.
-  - intros. apply CRzero_lt_one.
-  - intros. simpl. apply CRmult_lt_0_compat. exact H.
-    apply IHn. exact H.
+  intros. apply CR_complete in H. destruct H.
+  destruct (series_cv_maj u (fun k => CRabs R (u k)) x).
+  intro n. apply CRle_refl. assumption. exists x0. apply p.
 Qed.
 
-Lemma pow_mult : forall {R : ConstructiveReals} (x y : CRcarrier R) (n:nat),
-    CRpow x n * CRpow y n == CRpow (x*y) n.
+Lemma series_cv_unique :
+  forall {R : ConstructiveReals} (Un:nat -> CRcarrier R) (l1 l2:CRcarrier R),
+    series_cv Un l1 -> series_cv Un l2 -> l1 == l2.
 Proof.
-  induction n.
-  - simpl. rewrite CRmult_1_r. reflexivity.
-  - simpl. rewrite <- IHn. do 2 rewrite <- (Rmul_assoc (CRisRing R)).
-    apply CRmult_morph. reflexivity.
-    rewrite <- (Rmul_comm (CRisRing R)). rewrite <- (Rmul_assoc (CRisRing R)).
-    apply CRmult_morph. reflexivity.
-    rewrite <- (Rmul_comm (CRisRing R)). reflexivity.
+  intros. apply (CR_cv_unique (CRsum Un)); assumption.
 Qed.
 
-Lemma pow_one : forall {R : ConstructiveReals} (n:nat),
-    @CRpow R 1 n == 1.
+Lemma series_cv_abs_eq
+  : forall {R : ConstructiveReals} (u : nat -> CRcarrier R) (a : CRcarrier R)
+           (cau : CR_cauchy R (CRsum (fun n => CRabs R (u n)))),
+    series_cv u a
+    -> (a == (let (l,_):= series_cv_abs u cau in l))%ConstructiveReals.
 Proof.
-  induction n. reflexivity.
-  transitivity (CRmult R 1 (CRpow 1 n)). reflexivity.
-  rewrite IHn. rewrite CRmult_1_r. reflexivity.
+  intros. destruct (series_cv_abs u cau).
+  apply (series_cv_unique u). exact H. exact s.
 Qed.
 
-Lemma pow_proper : forall {R : ConstructiveReals} (x y : CRcarrier R) (n : nat),
-    x == y -> CRpow x n == CRpow y n.
+Lemma series_cv_abs_cv
+  : forall {R : ConstructiveReals} (u : nat -> CRcarrier R)
+           (cau : CR_cauchy R (CRsum (fun n => CRabs R (u n)))),
+    series_cv u (let (l,_):= series_cv_abs u cau in l).
 Proof.
-  induction n.
-  - intros. reflexivity.
-  - intros. simpl. rewrite IHn, H. reflexivity. exact H.
+  intros. destruct (series_cv_abs u cau). exact s.
+Qed.
+
+Lemma series_cv_opp : forall {R : ConstructiveReals}
+                        (s : CRcarrier R) (u : nat -> CRcarrier R),
+    series_cv u s
+    -> series_cv (fun n => - u n) (- s).
+Proof.
+  intros. intros p. specialize (H p) as [N H].
+  exists N. intros n H0.
+  setoid_replace (CRsum (fun n0 : nat => - u n0) n - - s)
+    with (-(CRsum (fun n0 : nat => u n0) n - s)).
+  rewrite CRabs_opp.
+  apply H, H0. unfold CRminus.
+  rewrite sum_opp. rewrite CRopp_plus_distr. reflexivity.
+Qed.
+
+Lemma series_cv_scale : forall {R : ConstructiveReals}
+                          (a : CRcarrier R) (s : CRcarrier R) (u : nat -> CRcarrier R),
+    series_cv u s
+    -> series_cv (fun n => (u n) * a) (s * a).
+Proof.
+  intros.
+  apply (CR_cv_eq _ (fun n => CRsum u n * a)).
+  intro n. rewrite sum_scale. reflexivity. apply CR_cv_scale, H.
+Qed.
+
+Lemma series_cv_plus : forall {R : ConstructiveReals}
+                         (u v : nat -> CRcarrier R) (s t : CRcarrier R),
+    series_cv u s
+    -> series_cv v t
+    -> series_cv (fun n => u n + v n) (s + t).
+Proof.
+  intros. apply (CR_cv_eq _ (fun n => CRsum u n + CRsum v n)).
+  intro n. symmetry. apply sum_plus. apply CR_cv_plus. exact H. exact H0.
+Qed.
+
+Lemma series_cv_minus : forall {R : ConstructiveReals}
+                          (u v : nat -> CRcarrier R) (s t : CRcarrier R),
+    series_cv u s
+    -> series_cv v t
+    -> series_cv (fun n => u n - v n) (s - t).
+Proof.
+  intros. apply (CR_cv_eq _ (fun n => CRsum u n - CRsum v n)).
+  intro n. symmetry. unfold CRminus. rewrite sum_plus.
+  rewrite sum_opp. reflexivity.
+  apply CR_cv_plus. exact H. apply CR_cv_opp. exact H0.
+Qed.
+
+Lemma series_cv_nonneg : forall {R : ConstructiveReals}
+                           (u : nat -> CRcarrier R) (s : CRcarrier R),
+    (forall n:nat, 0 <= u n) -> series_cv u s -> 0 <= s.
+Proof.
+  intros. apply (CRle_trans 0 (CRsum u 0)). apply H.
+  apply (growing_ineq (CRsum u)). intro n. simpl.
+  rewrite <- CRplus_0_r. apply CRplus_le_compat.
+  rewrite CRplus_0_r. apply CRle_refl. apply H. apply H0.
 Qed.
 
-Lemma pow_inv : forall {R : ConstructiveReals} (x : CRcarrier R) (xPos : 0 < x) (n : nat),
-    CRpow (CRinv R x (inr xPos)) n
-    == CRinv R (CRpow x n) (inr (pow_lt x n xPos)).
+Lemma series_cv_eq : forall {R : ConstructiveReals}
+                       (u v : nat -> CRcarrier R) (s : CRcarrier R),
+    (forall n:nat, u n == v n)
+    -> series_cv u s
+    -> series_cv v s.
+Proof.
+  intros. intros p. specialize (H0 p). destruct H0 as [N H0].
+  exists N. intros. unfold CRminus.
+  rewrite <- (CRsum_eq u). apply H0, H1. intros. apply H.
+Qed.
+
+Lemma series_cv_remainder_maj : forall {R : ConstructiveReals} (u : nat -> CRcarrier R)
+                                  (s eps : CRcarrier R)
+                                  (N : nat),
+    series_cv u s
+    -> 0 < eps
+    -> (forall n:nat, 0 <= u n)
+    -> CRabs R (CRsum u N - s) <= eps
+    -> forall n:nat, CRsum (fun k=> u (N + S k)%nat) n <= eps.
+Proof.
+  intros. pose proof (sum_assoc u N n).
+  rewrite <- (CRsum_eq (fun k : nat => u (S N + k)%nat)).
+  apply (CRplus_le_reg_l (CRsum u N)). rewrite <- H3.
+  apply (CRle_trans _ s). apply growing_ineq.
+  2: apply H.
+  intro k. simpl. rewrite <- CRplus_0_r, CRplus_assoc.
+  apply CRplus_le_compat_l. rewrite CRplus_0_l. apply H1.
+  rewrite CRabs_minus_sym in H2.
+  rewrite CRplus_comm. apply (CRplus_le_reg_r (-CRsum u N)).
+  rewrite CRplus_assoc. rewrite CRplus_opp_r. rewrite CRplus_0_r.
+  apply (CRle_trans _ (CRabs R (s - CRsum u N))). apply CRle_abs.
+  assumption. intros. rewrite Nat.add_succ_r. reflexivity.
+Qed.
+
+
+Lemma series_cv_abs_remainder : forall {R : ConstructiveReals} (u : nat -> CRcarrier R)
+                                  (s sAbs : CRcarrier R)
+                                  (n : nat),
+    series_cv u s
+    -> series_cv (fun n => CRabs R (u n)) sAbs
+    -> CRabs R (CRsum u n - s)
+      <= sAbs - CRsum (fun n => CRabs R (u n)) n.
+Proof.
+  intros.
+  apply (CR_cv_le (fun N => CRabs R (CRsum u n - (CRsum u (n + N))))
+                   (fun N => CRsum (fun n : nat => CRabs R (u n)) (n + N)
+                          - CRsum (fun n : nat => CRabs R (u n)) n)).
+  - intro N. destruct N. rewrite plus_0_r. unfold CRminus.
+    rewrite CRplus_opp_r. rewrite CRplus_opp_r.
+    rewrite CRabs_right. apply CRle_refl. apply CRle_refl.
+    rewrite Nat.add_succ_r.
+    replace (S (n + N)) with (S n + N)%nat. 2: reflexivity.
+    unfold CRminus. rewrite sum_assoc. rewrite sum_assoc.
+    rewrite CRopp_plus_distr.
+    rewrite <- CRplus_assoc, CRplus_opp_r, CRplus_0_l, CRabs_opp.
+    rewrite CRplus_comm, <- CRplus_assoc, CRplus_opp_l.
+    rewrite CRplus_0_l. apply multiTriangleIneg.
+  - apply CR_cv_dist_cont. intros eps.
+    specialize (H eps) as [N lim].
+    exists N. intros. rewrite plus_comm. apply lim. apply (le_trans N i).
+    assumption. rewrite <- (plus_0_r i). rewrite <- plus_assoc.
+    apply Nat.add_le_mono_l. apply le_0_n.
+  - apply CR_cv_plus. 2: apply CR_cv_const. intros eps.
+    specialize (H0 eps) as [N lim].
+    exists N. intros. rewrite plus_comm. apply lim. apply (le_trans N i).
+    assumption. rewrite <- (plus_0_r i). rewrite <- plus_assoc.
+    apply Nat.add_le_mono_l. apply le_0_n.
+Qed.
+
+Lemma series_cv_triangle : forall {R : ConstructiveReals}
+                             (u : nat -> CRcarrier R) (s sAbs : CRcarrier R),
+    series_cv u s
+    -> series_cv (fun n => CRabs R (u n)) sAbs
+    -> CRabs R s <= sAbs.
+Proof.
+  intros.
+  apply (CR_cv_le (fun n => CRabs R (CRsum u n))
+                   (CRsum (fun n => CRabs R (u n)))).
+  intros. apply multiTriangleIneg. apply CR_cv_abs_cont. assumption. assumption.
+Qed.
+
+Lemma series_cv_shift :
+  forall {R : ConstructiveReals} (f : nat -> CRcarrier R) k l,
+    series_cv (fun n => f (S k + n)%nat) l
+    -> series_cv f (l + CRsum f k).
+Proof.
+  intros. intro p. specialize (H p) as [n nmaj].
+  exists (S k+n)%nat. intros. destruct (Nat.le_exists_sub (S k) i).
+  apply (le_trans _ (S k + 0)). rewrite Nat.add_0_r. apply le_refl.
+  apply (le_trans _ (S k + n)). apply Nat.add_le_mono_l, le_0_n.
+  exact H. destruct H0. subst i.
+  rewrite Nat.add_comm in H. rewrite <- Nat.add_le_mono_r in H.
+  specialize (nmaj x H). unfold CRminus.
+  rewrite Nat.add_comm, (sum_assoc f k x).
+  setoid_replace (CRsum f k + CRsum (fun k0 : nat => f (S k + k0)%nat) x - (l + CRsum f k))
+    with (CRsum (fun k0 : nat => f (S k + k0)%nat) x - l).
+  exact nmaj. unfold CRminus. rewrite (CRplus_comm (CRsum f k)).
+  rewrite CRplus_assoc. apply CRplus_morph. reflexivity.
+  rewrite CRplus_comm, CRopp_plus_distr, CRplus_assoc.
+  rewrite CRplus_opp_l, CRplus_0_r. reflexivity.
+Qed.
+
+Lemma series_cv_shift' : forall {R : ConstructiveReals}
+                           (un : nat -> CRcarrier R) (s : CRcarrier R) (shift : nat),
+    series_cv un s
+    -> series_cv (fun n => un (n+shift)%nat)
+                       (s - match shift with
+                            | O => 0
+                            | S p => CRsum un p
+                            end).
+Proof.
+  intros. destruct shift as [|p].
+  - unfold CRminus. rewrite CRopp_0. rewrite CRplus_0_r.
+    apply (series_cv_eq un). intros.
+    rewrite plus_0_r. reflexivity. apply H.
+  - apply (CR_cv_eq _ (fun n => CRsum un (n + S p) - CRsum un p)).
+    intros. rewrite plus_comm. unfold CRminus.
+    rewrite sum_assoc. simpl. rewrite CRplus_comm, <- CRplus_assoc.
+    rewrite CRplus_opp_l, CRplus_0_l.
+    apply CRsum_eq. intros. rewrite (plus_comm i). reflexivity.
+    apply CR_cv_plus. apply (CR_cv_shift' _ (S p) _ H).
+    intros n. exists (Pos.to_nat n). intros.
+    unfold CRminus. simpl.
+    rewrite CRopp_involutive, CRplus_opp_l. rewrite CRabs_right.
+    apply CR_of_Q_le. discriminate. apply CRle_refl.
+Qed.
+
+Lemma CRmorph_sum : forall {R1 R2 : ConstructiveReals}
+                      (f : @ConstructiveRealsMorphism R1 R2)
+                      (un : nat -> CRcarrier R1) (n : nat),
+  CRmorph f (CRsum un n) ==
+  CRsum (fun n0 : nat => CRmorph f (un n0)) n.
 Proof.
   induction n.
-  - rewrite CRinv_1. reflexivity.
-  - transitivity (CRinv R x (inr xPos) * CRpow (CRinv R x (inr xPos)) n).
-    reflexivity. rewrite IHn.
-    assert (0 < x * CRpow x n).
-    { apply CRmult_lt_0_compat. exact xPos. apply pow_lt, xPos. }
-    rewrite <- (CRinv_mult_distr _ _ _ _ (inr H)).
-    apply CRinv_morph. reflexivity.
+  - reflexivity.
+  - simpl. rewrite CRmorph_plus, IHn. reflexivity.
 Qed.
 
-Lemma pow_plus_distr : forall {R : ConstructiveReals} (x : CRcarrier R) (n p:nat),
-    CRpow x n * CRpow x p == CRpow x (n+p).
+Lemma CRmorph_INR : forall {R1 R2 : ConstructiveReals}
+                      (f : @ConstructiveRealsMorphism R1 R2)
+                      (n : nat),
+  CRmorph f (INR n) == INR n.
 Proof.
   induction n.
-  - intros. simpl. rewrite CRmult_1_l. reflexivity.
-  - intros. simpl. rewrite CRmult_assoc. apply CRmult_morph.
-    reflexivity. apply IHn.
+  - apply CRmorph_rat.
+  - 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_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_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.
+Qed.
+
+Lemma CRmorph_series_cv : forall {R1 R2 : ConstructiveReals}
+                     (f : @ConstructiveRealsMorphism R1 R2)
+                     (un : nat -> CRcarrier R1)
+                     (l : CRcarrier R1),
+    series_cv un l
+    -> series_cv (fun n => CRmorph f (un n)) (CRmorph f l).
+Proof.
+  intros.
+  apply (CR_cv_eq _ (fun n => CRmorph f (CRsum un n))).
+  intro n. apply CRmorph_sum.
+  apply CRmorph_cv, H.
 Qed.
diff --git a/theories/Reals/Cauchy/ConstructiveCauchyAbs.v b/theories/Reals/Cauchy/ConstructiveCauchyAbs.v
index f8c6429982..10b435d8b0 100644
--- a/theories/Reals/Cauchy/ConstructiveCauchyAbs.v
+++ b/theories/Reals/Cauchy/ConstructiveCauchyAbs.v
@@ -20,6 +20,8 @@ Local Open Scope CReal_scope.
    The constructive formulation of the absolute value on the real numbers.
    This is followed by the constructive definitions of minimum and maximum,
    as min x y := (x + y - |x-y|) / 2.
+
+   WARNING: this file is experimental and likely to change in future releases.
 *)
 
 
diff --git a/theories/Reals/Cauchy/ConstructiveCauchyReals.v b/theories/Reals/Cauchy/ConstructiveCauchyReals.v
index 70574f6135..b332457a7b 100644
--- a/theories/Reals/Cauchy/ConstructiveCauchyReals.v
+++ b/theories/Reals/Cauchy/ConstructiveCauchyReals.v
@@ -39,6 +39,8 @@ Require CMorphisms.
 
     WARNING: this module is not meant to be imported directly,
     please import `Reals.Abstract.ConstructiveReals` instead.
+
+    WARNING: this file is experimental and likely to change in future releases.
  *)
 Definition QCauchySeq (un : positive -> Q)
   : Prop
diff --git a/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v b/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v
index f4daedcb97..7b7eb716e6 100644
--- a/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v
+++ b/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v
@@ -9,7 +9,10 @@
 (************************************************************************)
 (************************************************************************)
 
-(* The multiplication and division of Cauchy reals. *)
+(** The multiplication and division of Cauchy reals.
+
+    WARNING: this file is experimental and likely to change in future releases.
+*)
 
 Require Import QArith Qabs Qround.
 Require Import Logic.ConstructiveEpsilon.
diff --git a/theories/Reals/Cauchy/ConstructiveRcomplete.v b/theories/Reals/Cauchy/ConstructiveRcomplete.v
index 754f9be5fe..a6843d598c 100644
--- a/theories/Reals/Cauchy/ConstructiveRcomplete.v
+++ b/theories/Reals/Cauchy/ConstructiveRcomplete.v
@@ -16,6 +16,11 @@ Require Import ConstructiveCauchyRealsMult.
 Require Import Logic.ConstructiveEpsilon.
 Require Import ConstructiveCauchyAbs.
 
+(** Proof that Cauchy reals are Cauchy-complete.
+
+    WARNING: this file is experimental and likely to change in future releases.
+ *)
+
 Local Open Scope CReal_scope.
 
 (* We use <= in sort Prop rather than < in sort Set,
diff --git a/theories/Reals/ClassicalConstructiveReals.v b/theories/Reals/ClassicalConstructiveReals.v
new file mode 100644
index 0000000000..baeb937add
--- /dev/null
+++ b/theories/Reals/ClassicalConstructiveReals.v
@@ -0,0 +1,310 @@
+(************************************************************************)
+(*         *   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 classical reals are constructive reals with
+    extra properties, namely total order, existence of all
+    least upper bounds and setoid equivalence simplifying to
+    Leibniz equality.
+
+    From this point of view, the quotient Rabst and Rrepr
+    between classical Dedekind reals and constructive Cauchy reals
+    becomes an isomorphism for the ConstructiveReals structure.
+
+    This allows to apply results from constructive reals to
+    classical reals. *)
+
+Require Import QArith_base.
+Require Import Rdefinitions.
+Require Import Raxioms.
+Require Import ConstructiveReals.
+Require Import ConstructiveCauchyReals.
+Require Import ConstructiveCauchyRealsMult.
+Require Import ConstructiveRcomplete.
+Require Import ConstructiveCauchyAbs.
+Require Import ConstructiveRealsMorphisms.
+
+Local Open Scope R_scope.
+
+(* Rlt is the transport of CRealLt via Rasbt, Rrepr,
+   so it is linear as CRealLt. *)
+Lemma RisLinearOrder : isLinearOrder Rlt.
+Proof.
+  split. split.
+  - intros. exact (Rlt_asym _ _ H H0).
+  - intros. exact (Rlt_trans _ _ _ H H0).
+  - intros. destruct (total_order_T x y). destruct s.
+    left. exact r. right. subst x. exact H. right.
+    exact (Rlt_trans _ x _ r H).
+Qed.
+
+Lemma RdisjunctEpsilon
+  : forall a b c d : R, (a < b)%R \/ (c < d)%R -> (a < b)%R + (c < d)%R.
+Proof.
+  intros. destruct (total_order_T a b).
+  - destruct s.
+    left. exact r. right. destruct H.
+    exfalso. subst a. exact (Rlt_asym b b H H). exact H.
+  - right. destruct H. exfalso. exact (Rlt_asym _ _ H r). exact H.
+Qed.
+
+(* The constructive equality on R. *)
+Definition Req_constr (x y : R) : Prop
+  := (x < y -> False) /\ (y < x -> False).
+
+Lemma Req_constr_refl : forall x:R, Req_constr x x.
+Proof.
+  split. intro H. exact (Rlt_asym _ _ H H).
+  intro H. exact (Rlt_asym _ _ H H).
+Qed.
+
+Lemma Req_constr_leibniz : forall x y:R, Req_constr x y -> x = y.
+Proof.
+  intros. destruct (total_order_T x y). destruct s.
+  - exfalso. destruct H. contradiction.
+  - exact e.
+  - exfalso. destruct H. contradiction.
+Qed.
+
+Definition IQR (q : Q) := Rabst (inject_Q q).
+
+Lemma IQR_zero_quot : Req_constr (IQR 0) R0.
+Proof.
+  unfold IQR. rewrite R0_def. apply Req_constr_refl.
+Qed.
+
+(* Not RealField.RTheory, because it uses Leibniz equality. *)
+Lemma Rring : ring_theory (IQR 0) (IQR 1) Rplus Rmult
+                          (fun x y : R => (x + - y)%R) Ropp Req_constr.
+Proof.
+  split.
+  - intro x. replace (IQR 0 + x) with x. apply Req_constr_refl.
+    apply Rquot1. rewrite Rrepr_plus. unfold IQR. rewrite Rquot2.
+    rewrite CReal_plus_0_l. reflexivity.
+  - intros. replace (x + y) with (y + x). apply Req_constr_refl.
+    apply Rquot1. do 2 rewrite Rrepr_plus. apply CReal_plus_comm.
+  - intros. replace (x + (y + z)) with (x + y + z).
+    apply Req_constr_refl. apply Rquot1.
+    do 4 rewrite Rrepr_plus. apply CReal_plus_assoc.
+  - intro x. replace (IQR 1 * x) with x. apply Req_constr_refl.
+    unfold IQR.
+    apply Rquot1. rewrite Rrepr_mult, Rquot2, CReal_mult_1_l. reflexivity.
+  - intros. replace (x * y) with (y * x). apply Req_constr_refl.
+    apply Rquot1. do 2 rewrite Rrepr_mult. apply CReal_mult_comm.
+  - intros. replace (x * (y * z)) with (x * y * z).
+    apply Req_constr_refl. apply Rquot1.
+    do 4 rewrite Rrepr_mult. apply CReal_mult_assoc.
+  - intros. replace ((x + y) * z) with (x * z + y * z).
+    apply Req_constr_refl. apply Rquot1.
+    rewrite Rrepr_mult, Rrepr_plus, Rrepr_plus, Rrepr_mult, Rrepr_mult.
+    symmetry. apply CReal_mult_plus_distr_r.
+  - intros. apply Req_constr_refl.
+  - intros. replace (x + - x) with R0. unfold IQR.
+    rewrite R0_def. apply Req_constr_refl.
+    apply Rquot1. rewrite Rrepr_plus, Rrepr_opp, CReal_plus_opp_r, Rrepr_0.
+    reflexivity.
+Qed.
+
+Lemma RringExt : ring_eq_ext Rplus Rmult Ropp Req_constr.
+Proof.
+  split.
+  - intros x y H z t H0. apply Req_constr_leibniz in H.
+    apply Req_constr_leibniz in H0. destruct H, H0. apply Req_constr_refl.
+  - intros x y H z t H0. apply Req_constr_leibniz in H.
+    apply Req_constr_leibniz in H0. destruct H, H0. apply Req_constr_refl.
+  - intros x y H. apply Req_constr_leibniz in H. destruct H. apply Req_constr_refl.
+Qed.
+
+Lemma Rleft_inverse :
+  forall r : R, (sum (r < IQR 0) (IQR 0 < r)) -> Req_constr (/ r * r) (IQR 1).
+Proof.
+  intros. rewrite Rinv_l.
+  unfold IQR. rewrite <- R1_def. apply Req_constr_refl. destruct H.
+  - intro abs. subst r. unfold IQR in r0. rewrite <- R0_def in r0.
+    apply (Rlt_asym _ _ r0 r0).
+  - intro abs. subst r. unfold IQR in r0. rewrite <- R0_def in r0.
+    apply (Rlt_asym _ _ r0 r0).
+Qed.
+
+Lemma Rinv_pos : forall r : R, (sum (r < IQR 0) (IQR 0 < r)) -> IQR 0 < r -> IQR 0 < / r.
+Proof.
+  intros. rewrite Rlt_def. apply CRealLtForget.
+  rewrite Rlt_def in H0. apply CRealLtEpsilon in H0.
+  unfold IQR in H0. rewrite Rquot2 in H0.
+  rewrite (Rrepr_inv r (inr H0)). unfold IQR. rewrite Rquot2.
+  apply CReal_inv_0_lt_compat, H0.
+Qed.
+
+Lemma Rmult_pos : forall x y : R, IQR 0 < x -> IQR 0 < y -> IQR 0 < x * y.
+Proof.
+  intros. rewrite Rlt_def. apply CRealLtForget.
+  unfold IQR. rewrite Rquot2.
+  rewrite Rrepr_mult. apply CReal_mult_lt_0_compat.
+  rewrite Rlt_def in H. apply CRealLtEpsilon in H.
+  unfold IQR in H. rewrite Rquot2 in H. exact H.
+  unfold IQR in H0. rewrite Rlt_def in H0. apply CRealLtEpsilon in H0.
+  rewrite Rquot2 in H0. exact H0.
+Qed.
+
+Lemma Rplus_reg_l : forall r r1 r2, r + r1 < r + r2 -> r1 < r2.
+Proof.
+  intros. rewrite Rlt_def in H. apply CRealLtEpsilon in H.
+  rewrite Rrepr_plus, Rrepr_plus in H.
+  apply CReal_plus_lt_reg_l in H. rewrite Rlt_def.
+  apply CRealLtForget. exact H.
+Qed.
+
+Lemma Rzero_lt_one : IQR 0 < IQR 1.
+Proof.
+  rewrite Rlt_def. apply CRealLtForget.
+  unfold IQR. rewrite Rquot2, Rquot2.
+  apply CRealLt_0_1.
+Qed.
+
+Lemma plus_IQR : forall q r : Q,
+    IQR (q + r) = IQR q + IQR r.
+Proof.
+  intros. unfold IQR. apply Rquot1.
+  rewrite Rquot2, Rrepr_plus, Rquot2, Rquot2. apply inject_Q_plus.
+Qed.
+
+Lemma mult_IQR : forall q r : Q,
+    IQR (q * r) = IQR q * IQR r.
+Proof.
+  intros. unfold IQR. apply Rquot1.
+  rewrite Rquot2, Rrepr_mult, Rquot2, Rquot2. apply inject_Q_mult.
+Qed.
+
+Lemma IQR_lt : forall n m:Q, (n < m)%Q -> IQR n < IQR m.
+Proof.
+  intros. rewrite Rlt_def. apply CRealLtForget.
+  unfold IQR. rewrite Rquot2, Rquot2. apply inject_Q_lt, H.
+Qed.
+
+Lemma lt_IQR : forall n m:Q, IQR n < IQR m -> (n < m)%Q.
+Proof.
+  intros. rewrite Rlt_def in H. apply CRealLtEpsilon in H.
+  unfold IQR in H. rewrite Rquot2, Rquot2 in H.
+  apply lt_inject_Q, H.
+Qed.
+
+Lemma IQR_plus_quot : forall q r : Q, Req_constr (IQR (q + r)) (IQR q + IQR r).
+Proof.
+  intros. rewrite plus_IQR. apply Req_constr_refl.
+Qed.
+
+Lemma IQR_mult_quot : forall q r : Q, Req_constr (IQR (q * r)) (IQR q * IQR r).
+Proof.
+  intros. rewrite mult_IQR. apply Req_constr_refl.
+Qed.
+
+Lemma Rabove_pos : forall x : R, {n : positive & x < IQR (Z.pos n # 1)}.
+Proof.
+  intros. destruct (Rup_nat (Rrepr x)) as [n nmaj].
+  exists (Pos.of_nat n). unfold IQR. rewrite Rlt_def, Rquot2.
+  apply CRealLtForget. apply (CReal_lt_le_trans _ _ _ nmaj).
+  apply inject_Q_le. unfold Qle, Qnum, Qden.
+  do 2 rewrite Z.mul_1_r. destruct n. discriminate.
+  rewrite <- positive_nat_Z. rewrite Nat2Pos.id. apply Z.le_refl.
+  discriminate.
+Qed.
+
+Lemma Rarchimedean : forall x y : R, x < y -> {q : Q & ((x < IQR q) * (IQR q < y))%type}.
+Proof.
+  intros. rewrite Rlt_def in H. apply CRealLtEpsilon in H.
+  apply FQ_dense in H. destruct H as [q [H2 H3]].
+  exists q. split. rewrite Rlt_def. apply CRealLtForget.
+  unfold IQR. rewrite Rquot2. exact H2.
+  rewrite Rlt_def. apply CRealLtForget.
+  unfold IQR. rewrite Rquot2. exact H3.
+Qed.
+
+Lemma RabsLUB : forall x y : R, (y < x -> False) /\ (y < - x -> False) <-> (y < Rabst (CReal_abs (Rrepr x)) -> False).
+Proof.
+  split.
+  - intros. rewrite Rlt_def in H0.
+    apply CRealLtEpsilon in H0. rewrite Rquot2 in H0.
+    destruct H. apply (CReal_abs_le (Rrepr x) (Rrepr y)). 2: exact H0.
+    split. apply (CReal_plus_le_reg_l (Rrepr y - Rrepr x)).
+    ring_simplify. intro abs2. apply H1. rewrite Rlt_def.
+    apply CRealLtForget. rewrite Rrepr_opp. exact abs2.
+    intro abs2. apply H. rewrite Rlt_def.
+    apply CRealLtForget. exact abs2.
+  - intros. split. intro abs. apply H.
+    rewrite Rlt_def. apply CRealLtForget. rewrite Rquot2.
+    rewrite Rlt_def in abs. apply CRealLtEpsilon in abs.
+    apply (CReal_lt_le_trans _ _ _ abs). apply CReal_le_abs.
+    intro abs. apply H.
+    rewrite Rlt_def. apply CRealLtForget. rewrite Rquot2.
+    rewrite Rlt_def in abs. apply CRealLtEpsilon in abs.
+    apply (CReal_lt_le_trans _ _ _ abs).
+    rewrite <- CReal_abs_opp, Rrepr_opp. apply CReal_le_abs.
+Qed.
+
+Lemma Rcomplete : forall xn : nat -> R,
+  (forall p : positive,
+   {n : nat |
+   forall i j : nat,
+   (n <= i)%nat -> (n <= j)%nat -> IQR (1 # p) < Rabst (CReal_abs (Rrepr (xn i + - xn j))) -> False}) ->
+  {l : R &
+  forall p : positive,
+  {n : nat |
+  forall i : nat, (n <= i)%nat -> IQR (1 # p) < Rabst (CReal_abs (Rrepr (xn i + - l))) -> False}}.
+Proof.
+  intros. destruct (Rcauchy_complete (fun n => Rrepr (xn n))) as [l llim].
+  - intro p. specialize (H p) as [n nmaj]. exists n. intros.
+    specialize (nmaj i j H H0). unfold IQR in nmaj.
+    intro abs. apply nmaj. rewrite Rlt_def. apply CRealLtForget.
+    rewrite Rquot2, Rquot2. apply (CReal_lt_le_trans _ _ _ abs).
+    rewrite Rrepr_plus, Rrepr_opp. apply CRealLe_refl.
+  - exists (Rabst l). intros. specialize (llim p) as [n nmaj].
+    exists n. intros. specialize (nmaj i H0).
+    unfold IQR in H1. apply nmaj. rewrite Rlt_def in H1.
+    apply CRealLtEpsilon in H1. rewrite Rquot2, Rquot2 in H1.
+    apply (CReal_lt_le_trans _ _ _ H1).
+    rewrite Rrepr_plus, Rrepr_opp, Rquot2. apply CRealLe_refl.
+Qed.
+
+Definition Rabs_quot (x : R) := Rabst (CReal_abs (Rrepr x)).
+Definition Rinv_quot (x : R) (xnz : sum (x < IQR 0) (IQR 0 < x)) := Rinv x.
+Definition Rlt_epsilon (x y : R) (H : x < y) := H.
+
+Definition DRealConstructive : ConstructiveReals
+  := Build_ConstructiveReals
+       R Rlt RisLinearOrder Rlt
+       Rlt_epsilon Rlt_epsilon
+       RdisjunctEpsilon IQR IQR_lt lt_IQR
+       Rplus Ropp Rmult
+       IQR_plus_quot IQR_mult_quot
+       Rring RringExt Rzero_lt_one
+       Rplus_lt_compat_l Rplus_reg_l Rmult_pos
+       Rinv_quot Rleft_inverse Rinv_pos
+       Rarchimedean Rabove_pos
+       Rabs_quot RabsLUB Rcomplete.
+
+Definition Rrepr_morphism
+  : @ConstructiveRealsMorphism DRealConstructive CRealConstructive.
+Proof.
+  apply (Build_ConstructiveRealsMorphism
+           DRealConstructive CRealConstructive Rrepr).
+  - intro q. simpl. unfold IQR. rewrite Rquot2. apply CRealEq_refl.
+  - intros. simpl. simpl in H. rewrite Rlt_def in H.
+    apply CRealLtEpsilon in H. exact H.
+Defined.
+
+Definition Rabst_morphism
+  : @ConstructiveRealsMorphism CRealConstructive DRealConstructive.
+Proof.
+  apply (Build_ConstructiveRealsMorphism
+           CRealConstructive DRealConstructive Rabst).
+  - intro q. apply Req_constr_refl.
+  - intros. simpl. simpl in H. rewrite Rlt_def.
+    apply CRealLtForget. rewrite Rquot2, Rquot2. exact H.
+Defined.