Prove that classical reals implement constructive reals. Also move sums, min and max to CoRN.

Update stdlib index

Remove ConstructiveSum from the index

Add changelog entry

Make constructive reals experimental

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.