Merge PR #11725: Cleanup stdlib reals.

Ack-by: SkySkimmer
Reviewed-by: herbelin

6 files changed, 4970 insertions, 0 deletions

diff --git a/theories/Reals/Abstract/ConstructiveAbs.v b/theories/Reals/Abstract/ConstructiveAbs.v
new file mode 100644
index 0000000000..d357ad2d54
--- /dev/null
+++ b/theories/Reals/Abstract/ConstructiveAbs.v
@@ -0,0 +1,950 @@
+(************************************************************************)
+(*         *   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.
+
+Local Open Scope ConstructiveReals.
+
+(** Properties of constructive absolute value (defined in
+    ConstructiveReals.CRabs).
+    Definition of minimum, maximum and their properties. *)
+
+Instance CRabs_morph
+  : forall {R : ConstructiveReals},
+    CMorphisms.Proper
+      (CMorphisms.respectful (CReq R) (CReq R)) (CRabs R).
+Proof.
+  intros R x y [H H0]. split.
+  - rewrite <- CRabs_def. split.
+    + apply (CRle_trans _ x). apply H.
+      pose proof (CRabs_def R x (CRabs R x)) as [_ H1].
+      apply H1. apply CRle_refl.
+    + apply (CRle_trans _ (CRopp R x)). intro abs.
+      apply CRopp_lt_cancel in abs. contradiction.
+      pose proof (CRabs_def R x (CRabs R x)) as [_ H1].
+      apply H1. apply CRle_refl.
+  - rewrite <- CRabs_def. split.
+    + apply (CRle_trans _ y). apply H0.
+      pose proof (CRabs_def R y (CRabs R y)) as [_ H1].
+      apply H1. apply CRle_refl.
+    + apply (CRle_trans _ (CRopp R y)). intro abs.
+      apply CRopp_lt_cancel in abs. contradiction.
+      pose proof (CRabs_def R y (CRabs R y)) as [_ H1].
+      apply H1. apply CRle_refl.
+Qed.
+
+Add Parametric Morphism {R : ConstructiveReals} : (CRabs R)
+    with signature CReq R ==> CReq R
+      as CRabs_morph_prop.
+Proof.
+  intros. apply CRabs_morph, H.
+Qed.
+
+Lemma CRabs_right : forall {R : ConstructiveReals} (x : CRcarrier R),
+    0 <= x -> CRabs R x == x.
+Proof.
+  intros. split.
+  - pose proof (CRabs_def R x (CRabs R x)) as [_ H1].
+    apply H1, CRle_refl.
+  - rewrite <- CRabs_def. split. apply CRle_refl.
+    apply (CRle_trans _ (CRzero R)). 2: exact H.
+    apply (CRle_trans _ (CRopp R (CRzero R))).
+    intro abs. apply CRopp_lt_cancel in abs. contradiction.
+    apply (CRplus_le_reg_l (CRzero R)).
+    apply (CRle_trans _ (CRzero R)). apply CRplus_opp_r.
+    apply CRplus_0_r.
+Qed.
+
+Lemma CRabs_opp : forall {R : ConstructiveReals} (x : CRcarrier R),
+    CRabs R (- x) == CRabs R x.
+Proof.
+  intros. split.
+  - rewrite <- CRabs_def. split.
+    + pose proof (CRabs_def R (CRopp R x) (CRabs R (CRopp R x))) as [_ H1].
+      specialize (H1 (CRle_refl (CRabs R (CRopp R x)))) as [_ H1].
+      apply (CRle_trans _ (CRopp R (CRopp R x))).
+      2: exact H1. apply (CRopp_involutive x).
+    + pose proof (CRabs_def R (CRopp R x) (CRabs R (CRopp R x))) as [_ H1].
+      apply H1, CRle_refl.
+  - rewrite <- CRabs_def. split.
+    + pose proof (CRabs_def R x (CRabs R x)) as [_ H1].
+      apply H1, CRle_refl.
+    + apply (CRle_trans _ x). apply CRopp_involutive.
+      pose proof (CRabs_def R x (CRabs R x)) as [_ H1].
+      apply H1, CRle_refl.
+Qed.
+
+Lemma CRabs_minus_sym : forall {R : ConstructiveReals} (x y : CRcarrier R),
+    CRabs R (x - y) == CRabs R (y - x).
+Proof.
+  intros R x y. setoid_replace (x - y) with (-(y-x)).
+  rewrite CRabs_opp. reflexivity. unfold CRminus.
+  rewrite CRopp_plus_distr, CRplus_comm, CRopp_involutive.
+  reflexivity.
+Qed.
+
+Lemma CRabs_left : forall {R : ConstructiveReals} (x : CRcarrier R),
+    x <= 0 -> CRabs R x == - x.
+Proof.
+  intros. rewrite <- CRabs_opp. apply CRabs_right.
+  rewrite <- CRopp_0. apply CRopp_ge_le_contravar, H.
+Qed.
+
+Lemma CRabs_triang : forall {R : ConstructiveReals} (x y : CRcarrier R),
+    CRabs R (x + y) <= CRabs R x + CRabs R y.
+Proof.
+  intros. rewrite <- CRabs_def. split.
+  - apply (CRle_trans _ (CRplus R (CRabs R x) y)).
+    apply CRplus_le_compat_r.
+    pose proof (CRabs_def R x (CRabs R x)) as [_ H1].
+    apply H1, CRle_refl.
+    apply CRplus_le_compat_l.
+    pose proof (CRabs_def R y (CRabs R y)) as [_ H1].
+    apply H1, CRle_refl.
+  - apply (CRle_trans _ (CRplus R (CRopp R x) (CRopp R y))).
+    apply CRopp_plus_distr.
+    apply (CRle_trans _ (CRplus R (CRabs R x) (CRopp R y))).
+    apply CRplus_le_compat_r.
+    pose proof (CRabs_def R x (CRabs R x)) as [_ H1].
+    apply H1, CRle_refl.
+    apply CRplus_le_compat_l.
+    pose proof (CRabs_def R y (CRabs R y)) as [_ H1].
+    apply H1, CRle_refl.
+Qed.
+
+Lemma CRabs_le : forall {R : ConstructiveReals} (a b:CRcarrier R),
+    (-b <= a /\ a <= b) -> CRabs R a <= b.
+Proof.
+  intros. pose proof (CRabs_def R a b) as [H0 _].
+  apply H0. split. apply H. destruct H.
+  rewrite <- (CRopp_involutive b).
+  apply CRopp_ge_le_contravar. exact H.
+Qed.
+
+Lemma CRabs_triang_inv : forall {R : ConstructiveReals} (x y : CRcarrier R),
+    CRabs R x - CRabs R y <= CRabs R (x - y).
+Proof.
+  intros. apply (CRplus_le_reg_r (CRabs R y)).
+  unfold CRminus. rewrite CRplus_assoc, CRplus_opp_l.
+  rewrite CRplus_0_r.
+  apply (CRle_trans _ (CRabs R (x - y + y))).
+  setoid_replace (x - y + y) with x. apply CRle_refl.
+  unfold CRminus. rewrite CRplus_assoc, CRplus_opp_l.
+  rewrite CRplus_0_r. reflexivity.
+  apply CRabs_triang.
+Qed.
+
+Lemma CRabs_triang_inv2 : forall {R : ConstructiveReals} (x y : CRcarrier R),
+    CRabs R (CRabs R x - CRabs R y) <= CRabs R (x - y).
+Proof.
+  intros. apply CRabs_le. split.
+  2: apply CRabs_triang_inv.
+  apply (CRplus_le_reg_r (CRabs R y)).
+  unfold CRminus. rewrite CRplus_assoc, CRplus_opp_l.
+  rewrite CRplus_0_r. fold (x - y).
+  rewrite CRplus_comm, CRabs_minus_sym.
+  apply (CRle_trans _ _ _ (CRabs_triang_inv y (y-x))).
+  setoid_replace (y - (y - x)) with x. apply CRle_refl.
+  unfold CRminus. rewrite CRopp_plus_distr, <- CRplus_assoc.
+  rewrite CRplus_opp_r, CRplus_0_l. apply CRopp_involutive.
+Qed.
+
+Lemma CR_of_Q_abs : forall {R : ConstructiveReals} (q : Q),
+    CRabs R (CR_of_Q R q) == CR_of_Q R (Qabs q).
+Proof.
+  intros. destruct (Qlt_le_dec 0 q).
+  - apply (CReq_trans _ (CR_of_Q R q)).
+    apply CRabs_right. apply (CRle_trans _ (CR_of_Q R 0)).
+    apply CR_of_Q_zero. apply CR_of_Q_le. apply Qlt_le_weak, q0.
+    apply CR_of_Q_morph. symmetry. apply Qabs_pos, Qlt_le_weak, q0.
+  - apply (CReq_trans _ (CR_of_Q R (-q))).
+    apply (CReq_trans _ (CRabs R (CRopp R (CR_of_Q R q)))).
+    apply CReq_sym, CRabs_opp.
+    2: apply CR_of_Q_morph; symmetry; apply Qabs_neg, q0.
+    apply (CReq_trans _ (CRopp R (CR_of_Q R q))).
+    2: apply CReq_sym, CR_of_Q_opp.
+    apply CRabs_right. apply (CRle_trans _ (CR_of_Q R 0)).
+    apply CR_of_Q_zero.
+    apply (CRle_trans _ (CR_of_Q R (-q))). apply CR_of_Q_le.
+    apply (Qplus_le_l _ _ q). ring_simplify. exact q0.
+    apply CR_of_Q_opp.
+Qed.
+
+Lemma CRle_abs : forall {R : ConstructiveReals} (x : CRcarrier R),
+    x <= CRabs R x.
+Proof.
+  intros. pose proof (CRabs_def R x (CRabs R x)) as [_ H].
+  apply H, CRle_refl.
+Qed.
+
+Lemma CRabs_pos : forall {R : ConstructiveReals} (x : CRcarrier R),
+    0 <= CRabs R x.
+Proof.
+  intros. intro abs. destruct (CRltLinear R). clear p.
+  specialize (s _ x _ abs). destruct s.
+  exact (CRle_abs x c). rewrite CRabs_left in abs.
+  rewrite <- CRopp_0 in abs. apply CRopp_lt_cancel in abs.
+  exact (CRlt_asym _ _ abs c). apply CRlt_asym, c.
+Qed.
+
+Lemma CRabs_appart_0 : forall {R : ConstructiveReals} (x : CRcarrier R),
+    0 < CRabs R x -> x ≶ 0.
+Proof.
+  intros. destruct (CRltLinear R). clear p.
+  pose proof (s _ x _ H) as [pos|neg].
+  right. exact pos. left.
+  destruct (CR_Q_dense R _ _ neg) as [q [H0 H1]].
+  destruct (Qlt_le_dec 0 q).
+  - destruct (s (CR_of_Q R (-q)) x 0).
+    rewrite <- CR_of_Q_zero. apply CR_of_Q_lt.
+    apply (Qplus_lt_l _ _ q). ring_simplify. exact q0.
+    exfalso. pose proof (CRabs_def R x (CR_of_Q R q)) as [H2 _].
+    apply H2. clear H2. split. apply CRlt_asym, H0.
+    2: exact H1. rewrite <- Qopp_involutive, CR_of_Q_opp.
+    apply CRopp_ge_le_contravar, CRlt_asym, c. exact c.
+  - apply (CRlt_le_trans _ _ _ H0).
+    rewrite <- CR_of_Q_zero. apply CR_of_Q_le. exact q0.
+Qed.
+
+
+(* The proof by cases on the signs of x and y applies constructively,
+   because of the positivity hypotheses. *)
+Lemma CRabs_mult : forall {R : ConstructiveReals} (x y : CRcarrier R),
+    CRabs R (x * y) == CRabs R x * CRabs R y.
+Proof.
+  intro R.
+  assert (forall (x y : CRcarrier R),
+             x ≶ 0
+             -> y ≶ 0
+             -> CRabs R (x * y) == CRabs R x * CRabs R y) as prep.
+  { intros. destruct H, H0.
+    + rewrite CRabs_right, CRabs_left, CRabs_left.
+      rewrite <- CRopp_mult_distr_l, CRopp_mult_distr_r, CRopp_involutive.
+      reflexivity.
+      apply CRlt_asym, c0. apply CRlt_asym, c.
+      setoid_replace (x*y) with (- x * - y).
+      apply CRlt_asym, CRmult_lt_0_compat.
+      rewrite <- CRopp_0. apply CRopp_gt_lt_contravar, c.
+      rewrite <- CRopp_0. apply CRopp_gt_lt_contravar, c0.
+      rewrite <- CRopp_mult_distr_l, CRopp_mult_distr_r, CRopp_involutive.
+      reflexivity.
+    + rewrite CRabs_left, CRabs_left, CRabs_right.
+      rewrite <- CRopp_mult_distr_l. reflexivity.
+      apply CRlt_asym, c0. apply CRlt_asym, c.
+      rewrite <- (CRmult_0_l y).
+      apply CRmult_le_compat_r_half. exact c0.
+      apply CRlt_asym, c.
+    + rewrite CRabs_left, CRabs_right, CRabs_left.
+      rewrite <- CRopp_mult_distr_r. reflexivity.
+      apply CRlt_asym, c0. apply CRlt_asym, c.
+      rewrite <- (CRmult_0_r x).
+      apply CRmult_le_compat_l_half.
+      exact c. apply CRlt_asym, c0.
+    + rewrite CRabs_right, CRabs_right, CRabs_right. reflexivity.
+      apply CRlt_asym, c0. apply CRlt_asym, c.
+      apply CRlt_asym, CRmult_lt_0_compat; assumption. }
+  split.
+  - intro abs.
+    assert (0 < CRabs R x * CRabs R y).
+    { apply (CRle_lt_trans _ (CRabs R (x*y))).
+      apply CRabs_pos. exact abs. }
+    pose proof (CRmult_pos_appart_zero _ _ H).
+    rewrite CRmult_comm in H.
+    apply CRmult_pos_appart_zero in H.
+    destruct H. 2: apply (CRabs_pos y c).
+    destruct H0. 2: apply (CRabs_pos x c0).
+    apply CRabs_appart_0 in c.
+    apply CRabs_appart_0 in c0.
+    rewrite (prep x y) in abs.
+    exact (CRlt_asym _ _ abs abs). exact c0. exact c.
+  - intro abs.
+    assert (0 < CRabs R (x * y)).
+    { apply (CRle_lt_trans _ (CRabs R x * CRabs R y)).
+      rewrite <- (CRmult_0_l (CRabs R y)).
+      apply CRmult_le_compat_r.
+      apply CRabs_pos. apply CRabs_pos. exact abs. }
+    apply CRabs_appart_0 in H. destruct H.
+    + apply CRopp_gt_lt_contravar in c.
+      rewrite CRopp_0, CRopp_mult_distr_l in c.
+      pose proof (CRmult_pos_appart_zero _ _ c).
+      rewrite CRmult_comm in c.
+      apply CRmult_pos_appart_zero in c.
+      rewrite (prep x y) in abs.
+      exact (CRlt_asym _ _ abs abs).
+      destruct H. left. apply CRopp_gt_lt_contravar in c0.
+      rewrite CRopp_involutive, CRopp_0 in c0. exact c0.
+      right. apply CRopp_gt_lt_contravar in c0.
+      rewrite CRopp_involutive, CRopp_0 in c0. exact c0.
+      destruct c. right. exact c. left. exact c.
+    + pose proof (CRmult_pos_appart_zero _ _ c).
+      rewrite CRmult_comm in c.
+      apply CRmult_pos_appart_zero in c.
+      rewrite (prep x y) in abs.
+      exact (CRlt_asym _ _ abs abs).
+      destruct H. right. exact c0. left. exact c0.
+      destruct c. right. exact c. left. exact c.
+Qed.
+
+Lemma CRabs_lt : forall {R : ConstructiveReals} (x y : CRcarrier R),
+    CRabs _ x < y -> prod (x < y) (-x < y).
+Proof.
+  split.
+  - apply (CRle_lt_trans _ _ _ (CRle_abs x)), H.
+  - apply (CRle_lt_trans _ _ _ (CRle_abs (-x))).
+    rewrite CRabs_opp. exact H.
+Qed.
+
+Lemma CRabs_def1 : forall {R : ConstructiveReals} (x y : CRcarrier R),
+    x < y -> -x < y -> CRabs _ x < y.
+Proof.
+  intros. destruct (CRltLinear R), p.
+  destruct (s x (CRabs R x) y H). 2: exact c0.
+  rewrite CRabs_left. exact H0. intro abs.
+  rewrite CRabs_right in c0. exact (CRlt_asym x x c0 c0).
+  apply CRlt_asym, abs.
+Qed.
+
+Lemma CRabs_def2 : forall {R : ConstructiveReals} (x a:CRcarrier R),
+    CRabs _ x <= a -> (x <= a) /\ (- a <= x).
+Proof.
+  split.
+  - exact (CRle_trans _ _ _ (CRle_abs _) H).
+  - rewrite <- (CRopp_involutive x).
+    apply CRopp_ge_le_contravar.
+    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 CR_of_Q_one, CRmult_1_r.
+  rewrite (CR_of_Q_plus R 1 1), CR_of_Q_one, CRmult_plus_distr_l, CRmult_1_r.
+  rewrite CRabs_right. unfold CRminus.
+  rewrite CRopp_plus_distr, CRplus_assoc, <- (CRplus_assoc y).
+  rewrite CRplus_opp_r, CRplus_0_l, CRopp_involutive. reflexivity.
+  apply (CRmult_lt_compat_r (CR_of_Q R 2)) in H.
+  2: apply CR_of_Q_pos; reflexivity.
+  rewrite CRmult_assoc, <- CR_of_Q_mult in H.
+  setoid_replace ((1 # 2) * 2)%Q with 1%Q in H. 2: reflexivity.
+  rewrite CR_of_Q_one, CRmult_1_r in H.
+  rewrite CRmult_comm, (CR_of_Q_plus R 1 1), CR_of_Q_one, CRmult_plus_distr_r,
+  CRmult_1_l in H.
+  intro abs. rewrite CRabs_left in H.
+  unfold CRminus in H.
+  rewrite CRopp_involutive, CRplus_comm in H.
+  rewrite CRplus_assoc, <- (CRplus_assoc (-x)), CRplus_opp_l in H.
+  rewrite CRplus_0_l in H. exact (CRlt_asym _ _ H H).
+  apply CRlt_asym, abs.
+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)).
+  rewrite <- CR_of_Q_zero. apply CR_of_Q_lt; reflexivity.
+  rewrite CRmult_assoc, <- CR_of_Q_mult.
+  setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity.
+  rewrite CR_of_Q_one, CRmult_1_r.
+  rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CR_of_Q_one, CRmult_1_r.
+  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)).
+  rewrite <- CR_of_Q_zero. apply CR_of_Q_lt; reflexivity.
+  rewrite CRmult_assoc, <- CR_of_Q_mult.
+  setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity.
+  rewrite CR_of_Q_one, CRmult_1_r.
+  rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CR_of_Q_one, CRmult_1_r.
+  rewrite (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. rewrite <- CR_of_Q_zero. apply CR_of_Q_lt; reflexivity.
+  rewrite CRmult_plus_distr_r.
+  rewrite CRmult_assoc, <- CR_of_Q_mult.
+  setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity.
+  rewrite CR_of_Q_one, CRmult_1_r.
+  rewrite CRmult_assoc, <- CR_of_Q_mult.
+  setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity.
+  rewrite CR_of_Q_one, CRmult_1_r.
+  rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CR_of_Q_one, CRmult_1_r.
+  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. rewrite <- CR_of_Q_zero. apply CR_of_Q_lt; reflexivity.
+  rewrite CRmult_assoc, <- CR_of_Q_mult.
+  setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity.
+  rewrite CR_of_Q_one, CRmult_1_r.
+  rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CR_of_Q_one, CRmult_1_r.
+  rewrite 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. rewrite <- CR_of_Q_zero. apply CR_of_Q_lt; reflexivity.
+  rewrite CRmult_assoc, <- CR_of_Q_mult.
+  setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity.
+  rewrite CR_of_Q_one, CRmult_1_r.
+  rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CR_of_Q_one, CRmult_1_r.
+  rewrite 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)).
+  rewrite <- CR_of_Q_zero. apply CR_of_Q_lt; reflexivity.
+  rewrite CRmult_assoc, <- CR_of_Q_mult.
+  setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity.
+  rewrite CR_of_Q_one, CRmult_1_r.
+  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), CR_of_Q_one, 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), CR_of_Q_one, 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: rewrite <- CR_of_Q_zero; apply CR_of_Q_le; discriminate.
+  apply (CRle_trans _
+           ((CRabs _ (x - y) * 1 + CRabs _ (x-y) * 1)
+              * CR_of_Q R (1 # 2))).
+  apply CRmult_le_compat_r.
+  rewrite <- CR_of_Q_zero. apply CR_of_Q_le. discriminate.
+  apply (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, <- CR_of_Q_one.
+  rewrite <- (CR_of_Q_plus R 1 1).
+  rewrite CRmult_assoc, <- CR_of_Q_mult.
+  setoid_replace ((1 + 1) * (1 # 2))%Q with 1%Q. 2: reflexivity.
+  rewrite CR_of_Q_one, CRmult_1_r. apply CRle_refl.
+  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)).
+  rewrite <- CR_of_Q_zero. apply CR_of_Q_lt; reflexivity.
+  rewrite CRmult_assoc, <- CR_of_Q_mult.
+  setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity.
+  rewrite CR_of_Q_one, CRmult_1_r.
+  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), CR_of_Q_one, CRmult_plus_distr_l.
+    rewrite CRmult_1_r. apply CRplus_le_compat; exact H0.
+  - rewrite (CRplus_comm x), CRplus_assoc. apply CRplus_le_compat_l.
+    apply (CRplus_le_reg_l (-x)).
+    rewrite <- CRplus_assoc, CRplus_opp_l, CRplus_0_l.
+    rewrite CRopp_mult_distr_l.
+    rewrite (CR_of_Q_plus R 1 1), CR_of_Q_one, CRmult_plus_distr_l.
+    rewrite 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)). rewrite <- CR_of_Q_zero.
+  apply CR_of_Q_lt; reflexivity.
+  rewrite CRmult_assoc, <- CR_of_Q_mult.
+  setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity.
+  rewrite CR_of_Q_one, CRmult_1_r.
+  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, CR_of_Q_one, CRmult_1_r.
+    rewrite CRopp_plus_distr.
+    apply CRplus_le_compat; apply CRopp_ge_le_contravar; assumption.
+  - rewrite (CRplus_comm y), CRopp_plus_distr, CRplus_assoc.
+    apply CRplus_le_compat_l.
+    apply (CRplus_le_reg_l y).
+    rewrite <- CRplus_assoc, CRplus_opp_r, CRplus_0_l.
+    rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CR_of_Q_one, CRmult_1_r.
+    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)). rewrite <- CR_of_Q_zero.
+  apply CR_of_Q_lt; reflexivity.
+  rewrite CRmult_assoc, <- CR_of_Q_mult.
+  setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity.
+  rewrite CR_of_Q_one, CRmult_1_r.
+  setoid_replace 2%Q with (1+1)%Q. rewrite CR_of_Q_plus, CR_of_Q_one.
+  rewrite CRmult_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)). rewrite <- CR_of_Q_zero.
+  apply CR_of_Q_lt; reflexivity.
+  rewrite CRmult_assoc, <- CR_of_Q_mult.
+  setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity.
+  rewrite CR_of_Q_one, CRmult_1_r.
+  rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CR_of_Q_one, CRmult_1_r.
+  rewrite (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. rewrite <- CR_of_Q_zero. apply CR_of_Q_lt; reflexivity.
+  rewrite CRmult_plus_distr_r.
+  rewrite CRmult_assoc, <- CR_of_Q_mult.
+  setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity.
+  rewrite CR_of_Q_one, CRmult_1_r.
+  rewrite CRmult_assoc, <- CR_of_Q_mult.
+  setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity.
+  rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CR_of_Q_one, CRmult_1_r.
+  rewrite 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. rewrite <- CR_of_Q_zero. apply CR_of_Q_lt; reflexivity.
+  rewrite CRmult_assoc, <- CR_of_Q_mult.
+  setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity.
+  rewrite CR_of_Q_one, CRmult_1_r.
+  rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CR_of_Q_one, CRmult_1_r.
+  rewrite 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. rewrite <- CR_of_Q_zero. apply CR_of_Q_lt; reflexivity.
+  rewrite CRmult_assoc, <- CR_of_Q_mult.
+  setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity.
+  rewrite CR_of_Q_one, CRmult_1_r.
+  rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CR_of_Q_one, CRmult_1_r.
+  rewrite (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: rewrite <- CR_of_Q_zero; apply CR_of_Q_le; discriminate.
+  apply (CRle_trans
+           _ ((CRabs _ (x - y) * 1 + CRabs _ (x-y) * 1)
+              * CR_of_Q R (1 # 2))).
+  apply CRmult_le_compat_r.
+  rewrite <- CR_of_Q_zero. apply CR_of_Q_le. discriminate.
+  apply (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, <- CR_of_Q_one.
+  rewrite <- (CR_of_Q_plus R 1 1).
+  rewrite CRmult_assoc, <- CR_of_Q_mult.
+  setoid_replace ((1 + 1) * (1 # 2))%Q with 1%Q. 2: reflexivity.
+  rewrite CR_of_Q_one, CRmult_1_r. apply CRle_refl.
+  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)).
+  rewrite <- CR_of_Q_zero. apply CR_of_Q_lt; reflexivity.
+  rewrite CRmult_assoc, <- CR_of_Q_mult.
+  setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity.
+  rewrite CR_of_Q_one, CRmult_1_r.
+  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), CR_of_Q_one, CRmult_plus_distr_l.
+    rewrite CRmult_1_r. apply CRplus_le_lt_compat.
+    apply CRlt_asym, H0. exact H0.
+  - rewrite CRopp_plus_distr, CRopp_involutive.
+    rewrite CRplus_assoc. apply CRplus_lt_compat_l.
+    apply (CRplus_lt_reg_l _ x).
+    rewrite <- CRplus_assoc, CRplus_opp_r, CRplus_0_l.
+    rewrite (CR_of_Q_plus R 1 1), CR_of_Q_one, CRmult_plus_distr_l.
+    rewrite 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
new file mode 100644
index 0000000000..4ae24de154
--- /dev/null
+++ b/theories/Reals/Abstract/ConstructiveLUB.v
@@ -0,0 +1,413 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+(************************************************************************)
+
+(** Proof that LPO and the excluded middle for negations imply
+    the existence of least upper bounds for all non-empty and bounded
+    subsets of the real numbers. *)
+
+Require Import QArith_base Qabs.
+Require Import ConstructiveReals.
+Require Import ConstructiveAbs.
+Require Import ConstructiveLimits.
+Require Import Logic.ConstructiveEpsilon.
+
+Local Open Scope ConstructiveReals.
+
+Definition sig_forall_dec_T : Type
+  := forall (P : nat -> Prop), (forall n, {P n} + {~P n})
+                   -> {n | ~P n} + {forall n, P n}.
+
+Definition sig_not_dec_T : Type := forall P : Prop, { ~~P } + { ~P }.
+
+Definition is_upper_bound {R : ConstructiveReals}
+           (E:CRcarrier R -> Prop) (m:CRcarrier R)
+  := forall x:CRcarrier R, E x -> x <= m.
+
+Definition is_lub {R : ConstructiveReals}
+           (E:CRcarrier R -> Prop) (m:CRcarrier R) :=
+  is_upper_bound E m /\ (forall b:CRcarrier R, is_upper_bound E b -> m <= b).
+
+Lemma CRlt_lpo_dec : forall {R : ConstructiveReals} (x y : CRcarrier R),
+    (forall (P : nat -> Prop), (forall n, {P n} + {~P n})
+                    -> {n | ~P n} + {forall n, P n})
+    -> sum (x < y) (y <= x).
+Proof.
+  intros R x y lpo.
+  assert (forall (z:CRcarrier R) (n : nat), z < z + CR_of_Q R (1 # Pos.of_nat (S n))).
+  { intros. apply (CRle_lt_trans _ (z+0)).
+    rewrite CRplus_0_r. apply CRle_refl. apply CRplus_lt_compat_l.
+    apply CR_of_Q_pos. reflexivity. }
+  pose (fun n:nat => let (q,_) := CR_Q_dense
+                               R x (x + CR_of_Q R (1 # Pos.of_nat (S n))) (H x n)
+                in q)
+    as xn.
+  pose (fun n:nat => let (q,_) := CR_Q_dense
+                               R y (y + CR_of_Q R (1 # Pos.of_nat (S n))) (H y n)
+                in q)
+    as yn.
+  destruct (lpo (fun n => Qle (yn n) (xn n + (1 # Pos.of_nat (S n))))).
+  - intro n. destruct (Q_dec (yn n) (xn n + (1 # Pos.of_nat (S n)))).
+    destruct s. left. apply Qlt_le_weak, q.
+    right. apply (Qlt_not_le _ _ q). left.
+    rewrite q. apply Qle_refl.
+  - left. destruct s as [n nmaj]. apply Qnot_le_lt in nmaj.
+    apply (CRlt_le_trans _ (CR_of_Q R (xn n))).
+    unfold xn.
+    destruct (CR_Q_dense R x (x + CR_of_Q R (1 # Pos.of_nat (S n))) (H x n)).
+    exact (fst p). apply (CRle_trans _ (CR_of_Q R (yn n - (1 # Pos.of_nat (S n))))).
+    apply CR_of_Q_le. rewrite <- (Qplus_le_l _ _ (1# Pos.of_nat (S n))).
+    ring_simplify. apply Qlt_le_weak, nmaj.
+    unfold yn.
+    destruct (CR_Q_dense R y (y + CR_of_Q R (1 # Pos.of_nat (S n))) (H y n)).
+    unfold Qminus. rewrite CR_of_Q_plus, CR_of_Q_opp.
+    apply (CRplus_le_reg_r (CR_of_Q R (1 # Pos.of_nat (S n)))).
+    rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r.
+    apply CRlt_asym, (snd p).
+  - right. apply (CR_cv_le (fun n => CR_of_Q R (yn n))
+                           (fun n => CR_of_Q R (xn n) + CR_of_Q R (1 # Pos.of_nat (S n)))).
+    + intro n. rewrite <- CR_of_Q_plus. apply CR_of_Q_le. exact (q n).
+    + intro p. exists (Pos.to_nat p). intros.
+      unfold yn.
+      destruct (CR_Q_dense R y (y + CR_of_Q R (1 # Pos.of_nat (S i))) (H y i)).
+      rewrite CRabs_right. apply (CRplus_le_reg_r y).
+      unfold CRminus. rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r.
+      rewrite CRplus_comm.
+      apply (CRle_trans _ (y + CR_of_Q R (1 # Pos.of_nat (S i)))).
+      apply CRlt_asym, (snd p0). apply CRplus_le_compat_l.
+      apply CR_of_Q_le. unfold Qle, Qnum, Qden.
+      rewrite Z.mul_1_l, Z.mul_1_l. apply Pos2Z.pos_le_pos.
+      apply Pos2Nat.inj_le. rewrite Nat2Pos.id.
+      apply le_S, H0. discriminate. rewrite <- (CRplus_opp_r y).
+      apply CRplus_le_compat_r, CRlt_asym, p0.
+    + apply (CR_cv_proper _ (x+0)). 2: rewrite CRplus_0_r; reflexivity.
+      apply CR_cv_plus.
+      intro p. exists (Pos.to_nat p). intros.
+      unfold xn.
+      destruct (CR_Q_dense R x (x + CR_of_Q R (1 # Pos.of_nat (S i))) (H x i)).
+      rewrite CRabs_right. apply (CRplus_le_reg_r x).
+      unfold CRminus. rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r.
+      rewrite CRplus_comm.
+      apply (CRle_trans _ (x + CR_of_Q R (1 # Pos.of_nat (S i)))).
+      apply CRlt_asym, (snd p0). apply CRplus_le_compat_l.
+      apply CR_of_Q_le. unfold Qle, Qnum, Qden.
+      rewrite Z.mul_1_l, Z.mul_1_l. apply Pos2Z.pos_le_pos.
+      apply Pos2Nat.inj_le. rewrite Nat2Pos.id.
+      apply le_S, H0. discriminate. rewrite <- (CRplus_opp_r x).
+      apply CRplus_le_compat_r, CRlt_asym, p0.
+      intro p. exists (Pos.to_nat p). intros.
+      unfold CRminus. rewrite CRopp_0, CRplus_0_r, CRabs_right.
+      apply CR_of_Q_le. unfold Qle, Qnum, Qden.
+      rewrite Z.mul_1_l, Z.mul_1_l. apply Pos2Z.pos_le_pos.
+      apply Pos2Nat.inj_le. rewrite Nat2Pos.id.
+      apply le_S, H0. discriminate.
+      rewrite <- CR_of_Q_zero. apply CR_of_Q_le. discriminate.
+Qed.
+
+Lemma is_upper_bound_dec :
+  forall {R : ConstructiveReals} (E:CRcarrier R -> Prop) (x:CRcarrier R),
+    sig_forall_dec_T
+    -> sig_not_dec_T
+    -> { is_upper_bound E x } + { ~is_upper_bound E x }.
+Proof.
+  intros R E x lpo sig_not_dec.
+  destruct (sig_not_dec (~exists y:CRcarrier R, E y /\ CRltProp R x y)).
+  - left. intros y H.
+    destruct (CRlt_lpo_dec x y lpo). 2: exact c.
+    exfalso. apply n. intro abs. apply abs. clear abs.
+    exists y. split. exact H. apply CRltForget. exact c.
+  - right. intro abs. apply n. intros [y [H H0]].
+    specialize (abs y H). apply CRltEpsilon in H0. contradiction.
+Qed.
+
+Lemma is_upper_bound_epsilon :
+  forall {R : ConstructiveReals} (E:CRcarrier R -> Prop),
+    sig_forall_dec_T
+    -> sig_not_dec_T
+    -> (exists x:CRcarrier R, is_upper_bound E x)
+    -> { n:nat | is_upper_bound E (CR_of_Q R (Z.of_nat n # 1)) }.
+Proof.
+  intros R E lpo sig_not_dec Ebound.
+  apply constructive_indefinite_ground_description_nat.
+  - intro n. apply is_upper_bound_dec. exact lpo. exact sig_not_dec.
+  - destruct Ebound as [x H]. destruct (CRup_nat x) as [n nmaj]. exists n.
+    intros y ey. specialize (H y ey).
+    apply (CRle_trans _ x _ H). apply CRlt_asym, nmaj.
+Qed.
+
+Lemma is_upper_bound_not_epsilon :
+  forall {R : ConstructiveReals} (E:CRcarrier R -> Prop),
+    sig_forall_dec_T
+    -> sig_not_dec_T
+    -> (exists x : CRcarrier R, E x)
+    -> { m:nat | ~is_upper_bound E (-CR_of_Q R (Z.of_nat m # 1)) }.
+Proof.
+  intros R E lpo sig_not_dec H.
+  apply constructive_indefinite_ground_description_nat.
+  - intro n.
+    destruct (is_upper_bound_dec E (-CR_of_Q R (Z.of_nat n # 1)) lpo sig_not_dec).
+    right. intro abs. contradiction. left. exact n0.
+  - destruct H as [x H]. destruct (CRup_nat (-x)) as [n H0].
+    exists n. intro abs. specialize (abs x H).
+    apply abs. rewrite <- (CRopp_involutive x).
+    apply CRopp_gt_lt_contravar. exact H0.
+Qed.
+
+(* Decidable Dedekind cuts are Cauchy reals. *)
+Record DedekindDecCut : Type :=
+  {
+    DDupcut : Q -> Prop;
+    DDproper : forall q r : Q, (q == r -> DDupcut q -> DDupcut r)%Q;
+    DDlow : Q;
+    DDhigh : Q;
+    DDdec : forall q:Q, { DDupcut q } + { ~DDupcut q };
+    DDinterval : forall q r : Q, Qle q r -> DDupcut q -> DDupcut r;
+    DDhighProp : DDupcut DDhigh;
+    DDlowProp : ~DDupcut DDlow;
+  }.
+
+Lemma DDlow_below_up : forall (upcut : DedekindDecCut) (a b : Q),
+    DDupcut upcut a -> ~DDupcut upcut b -> Qlt b a.
+Proof.
+  intros. destruct (Qlt_le_dec b a). exact q.
+  exfalso. apply H0. apply (DDinterval upcut a).
+  exact q. exact H.
+Qed.
+
+Fixpoint DDcut_limit_fix (upcut : DedekindDecCut) (r : Q) (n : nat) :
+  Qlt 0 r
+  -> (DDupcut upcut (DDlow upcut + (Z.of_nat n#1) * r))
+  -> { q : Q | DDupcut upcut q /\ ~DDupcut upcut (q - r) }.
+Proof.
+  destruct n.
+  - intros. exfalso. simpl in H0.
+    apply (DDproper upcut _ (DDlow upcut)) in H0. 2: ring.
+    exact (DDlowProp upcut H0).
+  - intros. destruct (DDdec upcut (DDlow upcut + (Z.of_nat n # 1) * r)).
+    + exact (DDcut_limit_fix upcut r n H d).
+    + exists (DDlow upcut + (Z.of_nat (S n) # 1) * r)%Q. split.
+      exact H0. intro abs.
+      apply (DDproper upcut _ (DDlow upcut + (Z.of_nat n # 1) * r)) in abs.
+      contradiction.
+      rewrite Nat2Z.inj_succ. unfold Z.succ. rewrite <- Qinv_plus_distr.
+      ring.
+Qed.
+
+Lemma DDcut_limit : forall (upcut : DedekindDecCut) (r : Q),
+  Qlt 0 r
+  -> { q : Q | DDupcut upcut q /\ ~DDupcut upcut (q - r) }.
+Proof.
+  intros.
+  destruct (Qarchimedean ((DDhigh upcut - DDlow upcut)/r)) as [n nmaj].
+  apply (DDcut_limit_fix upcut r (Pos.to_nat n) H).
+  apply (Qmult_lt_r _ _ r) in nmaj. 2: exact H.
+  unfold Qdiv in nmaj.
+  rewrite <- Qmult_assoc, (Qmult_comm (/r)), Qmult_inv_r, Qmult_1_r in nmaj.
+  apply (DDinterval upcut (DDhigh upcut)). 2: exact (DDhighProp upcut).
+  apply Qlt_le_weak. apply (Qplus_lt_r _ _ (-DDlow upcut)).
+  rewrite Qplus_assoc, <- (Qplus_comm (DDlow upcut)), Qplus_opp_r,
+  Qplus_0_l, Qplus_comm.
+  rewrite positive_nat_Z. exact nmaj.
+  intros abs. rewrite abs in H. exact (Qlt_irrefl 0 H).
+Qed.
+
+Lemma glb_dec_Q : forall {R : ConstructiveReals} (upcut : DedekindDecCut),
+    { x : CRcarrier R
+    | forall r:Q, (x < CR_of_Q R r -> DDupcut upcut r)
+             /\ (CR_of_Q R r < x -> ~DDupcut upcut r) }.
+Proof.
+  intros.
+  assert (forall a b : Q, Qle a b -> Qle (-b) (-a)).
+  { intros. apply (Qplus_le_l _ _ (a+b)). ring_simplify. exact H. }
+  assert (CR_cauchy R (fun n:nat => CR_of_Q R (proj1_sig (DDcut_limit
+                                           upcut (1#Pos.of_nat n) (eq_refl _))))).
+  { intros p. exists (Pos.to_nat p). intros i j pi pj.
+    destruct (DDcut_limit upcut (1 # Pos.of_nat i) eq_refl),
+    (DDcut_limit upcut (1 # Pos.of_nat j) eq_refl); unfold proj1_sig.
+    apply (CRabs_le). split.
+    - intros. unfold CRminus.
+      rewrite <- CR_of_Q_opp, <- CR_of_Q_opp, <- CR_of_Q_plus.
+      apply CR_of_Q_le.
+      apply (Qplus_le_l _ _ x0). ring_simplify.
+      setoid_replace (-1 * (1 # p) + x0)%Q with (x0 - (1 # p))%Q.
+      2: ring. apply (Qle_trans _ (x0- (1#Pos.of_nat j))).
+      apply Qplus_le_r. apply H.
+      apply Z2Nat.inj_le. discriminate. discriminate. simpl.
+      rewrite Nat2Pos.id. exact pj. intro abs.
+      subst j. inversion pj. pose proof (Pos2Nat.is_pos p).
+      rewrite H1 in H0. inversion H0.
+      apply Qlt_le_weak, (DDlow_below_up upcut). apply a. apply a0.
+    - unfold CRminus. rewrite <- CR_of_Q_opp, <- CR_of_Q_plus.
+      apply CR_of_Q_le.
+      apply (Qplus_le_l _ _ (x0-(1#p))). ring_simplify.
+      setoid_replace (x -1 * (1 # p))%Q with (x - (1 # p))%Q.
+      2: ring. apply (Qle_trans _ (x- (1#Pos.of_nat i))).
+      apply Qplus_le_r. apply H.
+      apply Z2Nat.inj_le. discriminate. discriminate. simpl.
+      rewrite Nat2Pos.id. exact pi. intro abs.
+      subst i. inversion pi. pose proof (Pos2Nat.is_pos p).
+      rewrite H1 in H0. inversion H0.
+      apply Qlt_le_weak, (DDlow_below_up upcut). apply a0. apply a. }
+  apply CR_complete in H0. destruct H0 as [l lcv].
+  exists l. split.
+  - intros. (* find an upper point between the limit and r *)
+    destruct (CR_cv_open_above _ (CR_of_Q R r) l lcv H0) as [p pmaj].
+    specialize (pmaj p (le_refl p)).
+    unfold proj1_sig in pmaj.
+    destruct (DDcut_limit upcut (1 # Pos.of_nat p) eq_refl) as [q qmaj].
+    apply (DDinterval upcut q). 2: apply qmaj.
+    destruct (Q_dec q r). destruct s. apply Qlt_le_weak, q0.
+    exfalso. apply (CR_of_Q_lt R) in q0. exact (CRlt_asym _ _ pmaj q0).
+    rewrite q0. apply Qle_refl.
+  - intros H0 abs.
+    assert ((CR_of_Q R r+l) * CR_of_Q R (1#2) < l).
+    { apply (CRmult_lt_reg_r (CR_of_Q R 2)).
+      apply CR_of_Q_pos. reflexivity.
+      rewrite CRmult_assoc, <- CR_of_Q_mult, (CR_of_Q_plus R 1 1).
+      setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity.
+      rewrite CR_of_Q_one, CRmult_plus_distr_l, CRmult_1_r, CRmult_1_r.
+      apply CRplus_lt_compat_r. exact H0. }
+    destruct (CR_cv_open_below _ _ l lcv H1) as [p pmaj].
+    assert (0 < (l-CR_of_Q R r) * CR_of_Q R (1#2)).
+    { apply CRmult_lt_0_compat. rewrite <- (CRplus_opp_r (CR_of_Q R r)).
+      apply CRplus_lt_compat_r. exact H0. apply CR_of_Q_pos. reflexivity. }
+    destruct (CRup_nat (CRinv R _ (inr H2))) as [i imaj].
+    destruct i. exfalso. simpl in imaj.
+    rewrite CR_of_Q_zero in imaj.
+    exact (CRlt_asym _ _ imaj (CRinv_0_lt_compat R _ (inr H2) H2)).
+    specialize (pmaj (max (S i) (S p)) (le_trans p (S p) _ (le_S p p (le_refl p)) (Nat.le_max_r (S i) (S p)))).
+    unfold proj1_sig in pmaj.
+    destruct (DDcut_limit upcut (1 # Pos.of_nat (max (S i) (S p))) eq_refl)
+      as [q qmaj].
+    destruct qmaj. apply H4. clear H4.
+    apply (DDinterval upcut r). 2: exact abs.
+    apply (Qplus_le_l _ _ (1 # Pos.of_nat (Init.Nat.max (S i) (S p)))).
+    ring_simplify. apply (Qle_trans _ (r + (1 # Pos.of_nat (S i)))).
+    rewrite Qplus_le_r. unfold Qle,Qnum,Qden.
+    rewrite Z.mul_1_l, Z.mul_1_l. apply Pos2Z.pos_le_pos.
+    apply Pos2Nat.inj_le. rewrite Nat2Pos.id, Nat2Pos.id.
+    apply Nat.le_max_l. discriminate. discriminate.
+    apply (CRmult_lt_compat_l ((l - CR_of_Q R r) * CR_of_Q R (1 # 2))) in imaj.
+    rewrite CRinv_r in imaj. 2: exact H2.
+    destruct (Q_dec (r+(1#Pos.of_nat (S i))) q). destruct s.
+    apply Qlt_le_weak, q0. 2: rewrite q0; apply Qle_refl.
+    exfalso. apply (CR_of_Q_lt R) in q0.
+    apply (CRlt_asym _ _ pmaj). apply (CRlt_le_trans _ _ _ q0).
+    apply (CRplus_le_reg_l (-CR_of_Q R r)).
+    rewrite CR_of_Q_plus, <- CRplus_assoc, CRplus_opp_l, CRplus_0_l.
+    apply (CRmult_lt_compat_r (CR_of_Q R (1 # Pos.of_nat (S i)))) in imaj.
+    rewrite CRmult_1_l in imaj.
+    apply (CRle_trans _ (
+         (l - CR_of_Q R r) * CR_of_Q R (1 # 2) * CR_of_Q R (Z.of_nat (S i) # 1) *
+         CR_of_Q R (1 # Pos.of_nat (S i)))).
+    apply CRlt_asym, imaj. rewrite CRmult_assoc, <- CR_of_Q_mult.
+    setoid_replace ((Z.of_nat (S i) # 1) * (1 # Pos.of_nat (S i)))%Q with 1%Q.
+    rewrite CR_of_Q_one, CRmult_1_r.
+    unfold CRminus. rewrite CRmult_plus_distr_r, (CRplus_comm (-CR_of_Q R r)).
+    rewrite (CRplus_comm (CR_of_Q R r)), CRmult_plus_distr_r.
+    rewrite CRplus_assoc. apply CRplus_le_compat_l.
+    rewrite <- CR_of_Q_mult, <- CR_of_Q_opp, <- CR_of_Q_mult, <- CR_of_Q_plus.
+    apply CR_of_Q_le. ring_simplify. apply Qle_refl.
+    unfold Qeq, Qmult, Qnum, Qden. rewrite Z.mul_1_r, Z.mul_1_r.
+    rewrite Z.mul_1_l, Pos.mul_1_l. unfold Z.of_nat.
+    apply f_equal. apply Pos.of_nat_succ. apply CR_of_Q_pos. reflexivity.
+Qed.
+
+Lemma is_upper_bound_glb :
+  forall {R : ConstructiveReals} (E:CRcarrier R -> Prop),
+    sig_not_dec_T
+    -> sig_forall_dec_T
+    -> (exists x : CRcarrier R, E x)
+    -> (exists x : CRcarrier R, is_upper_bound E x)
+    -> { x : CRcarrier R
+      | forall r:Q, (x < CR_of_Q R r -> is_upper_bound E (CR_of_Q R r))
+               /\ (CR_of_Q R r < x -> ~is_upper_bound E (CR_of_Q R r)) }.
+Proof.
+  intros R E sig_not_dec lpo Einhab Ebound.
+  destruct (is_upper_bound_epsilon E lpo sig_not_dec Ebound) as [a luba].
+  destruct (is_upper_bound_not_epsilon E lpo sig_not_dec Einhab) as [b glbb].
+  pose (fun q => is_upper_bound E (CR_of_Q R q)) as upcut.
+  assert (forall q:Q, { upcut q } + { ~upcut q } ).
+  { intro q. apply is_upper_bound_dec. exact lpo. exact sig_not_dec. }
+  assert (forall q r : Q, (q <= r)%Q -> upcut q -> upcut r).
+  { intros. intros x Ex. specialize (H1 x Ex). intro abs.
+    apply H1. apply (CRle_lt_trans _ (CR_of_Q R r)). 2: exact abs.
+    apply CR_of_Q_le. exact H0. }
+  assert (upcut (Z.of_nat a # 1)%Q).
+  { intros x Ex. exact (luba x Ex). }
+  assert (~upcut (- Z.of_nat b # 1)%Q).
+  { intros abs. apply glbb. intros x Ex.
+    specialize (abs x Ex). rewrite <- CR_of_Q_opp.
+    exact abs. }
+  assert (forall q r : Q, (q == r)%Q -> upcut q -> upcut r).
+  { intros. intros x Ex. specialize (H4 x Ex). rewrite <- H3. exact H4. }
+  destruct (@glb_dec_Q R (Build_DedekindDecCut
+                            upcut H3 (-Z.of_nat b # 1)%Q (Z.of_nat a # 1)
+                            H H0 H1 H2)).
+  simpl in a0. exists x. intro r. split.
+  - intros. apply a0. exact H4.
+  - intros H6 abs. specialize (a0 r) as [_ a0]. apply a0.
+    exact H6. exact abs.
+Qed.
+
+Lemma is_upper_bound_closed :
+  forall {R : ConstructiveReals}
+    (E:CRcarrier R -> Prop) (sig_forall_dec : sig_forall_dec_T)
+    (sig_not_dec : sig_not_dec_T)
+    (Einhab : exists x : CRcarrier R, E x)
+    (Ebound : exists x : CRcarrier R, is_upper_bound E x),
+    is_lub
+      E (proj1_sig (is_upper_bound_glb
+                      E sig_not_dec sig_forall_dec Einhab Ebound)).
+Proof.
+  intros. split.
+  - intros x Ex.
+    destruct (is_upper_bound_glb E sig_not_dec sig_forall_dec Einhab Ebound); simpl.
+    intro abs. destruct (CR_Q_dense R x0 x abs) as [q [qmaj H]].
+    specialize (a q) as [a _]. specialize (a qmaj x Ex).
+    contradiction.
+  - intros.
+    destruct (is_upper_bound_glb E sig_not_dec sig_forall_dec Einhab Ebound); simpl.
+    intro abs. destruct (CR_Q_dense R b x abs) as [q [qmaj H0]].
+    specialize (a q) as [_ a]. apply a. exact H0.
+    intros y Ey. specialize (H y Ey). intro abs2.
+    apply H. exact (CRlt_trans _ (CR_of_Q R q) _ qmaj abs2).
+Qed.
+
+Lemma sig_lub :
+  forall {R : ConstructiveReals} (E:CRcarrier R -> Prop),
+    sig_forall_dec_T
+    -> sig_not_dec_T
+    -> (exists x : CRcarrier R, E x)
+    -> (exists x : CRcarrier R, is_upper_bound E x)
+    -> { u : CRcarrier R | is_lub E u }.
+Proof.
+  intros R E sig_forall_dec sig_not_dec Einhab Ebound.
+  pose proof (is_upper_bound_closed E sig_forall_dec sig_not_dec Einhab Ebound).
+  destruct (is_upper_bound_glb
+              E sig_not_dec sig_forall_dec Einhab Ebound); simpl in H.
+  exists x. exact H.
+Qed.
+
+Definition CRis_upper_bound {R : ConstructiveReals} (E:CRcarrier R -> Prop) (m:CRcarrier R)
+  := forall x:CRcarrier R, E x -> CRlt R m x -> False.
+
+Lemma CR_sig_lub :
+  forall {R : ConstructiveReals} (E:CRcarrier R -> Prop),
+    (forall x y : CRcarrier R, CReq R x y -> (E x <-> E y))
+    -> sig_forall_dec_T
+    -> sig_not_dec_T
+    -> (exists x : CRcarrier R, E x)
+    -> (exists x : CRcarrier R, CRis_upper_bound E x)
+    -> { u : CRcarrier R | CRis_upper_bound E u /\
+                           forall y:CRcarrier R, CRis_upper_bound E y -> CRlt R y u -> False }.
+Proof.
+  intros. exact (sig_lub E X X0 H0 H1).
+Qed.
diff --git a/theories/Reals/Abstract/ConstructiveLimits.v b/theories/Reals/Abstract/ConstructiveLimits.v
new file mode 100644
index 0000000000..4a40cc8cb3
--- /dev/null
+++ b/theories/Reals/Abstract/ConstructiveLimits.v
@@ -0,0 +1,933 @@
+(************************************************************************)
+(*         *   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 ConstructiveAbs.
+Require Import ConstructiveSum.
+
+Local Open Scope ConstructiveReals.
+
+
+(** Definitions and basic properties of limits of real sequences
+    and series. *)
+
+
+Lemma CR_cv_extens
+  : forall {R : ConstructiveReals} (xn yn : nat -> CRcarrier R) (l : CRcarrier R),
+    (forall n:nat, xn n == yn n)
+    -> CR_cv R xn l
+    -> CR_cv R yn l.
+Proof.
+  intros. intro p. specialize (H0 p) as [n nmaj]. exists n.
+  intros. specialize (nmaj i H0).
+  apply (CRle_trans _ (CRabs R (CRminus R (xn i) l))).
+  2: exact nmaj. rewrite <- CRabs_def. split.
+  - apply (CRle_trans _ (CRminus R (xn i) l)).
+    apply CRplus_le_compat_r. specialize (H i) as [H _]. exact H.
+    pose proof (CRabs_def R (CRminus R (xn i) l) (CRabs R (CRminus R (xn i) l)))
+      as [_ H1].
+    apply H1. apply CRle_refl.
+  - apply (CRle_trans _ (CRopp R (CRminus R (xn i) l))).
+    intro abs. apply CRopp_lt_cancel, CRplus_lt_reg_r in abs.
+    specialize (H i) as [_ H]. contradiction.
+    pose proof (CRabs_def R (CRminus R (xn i) l) (CRabs R (CRminus R (xn i) l)))
+      as [_ H1].
+    apply H1. apply CRle_refl.
+Qed.
+
+Lemma CR_cv_opp : forall {R : ConstructiveReals} (xn : nat -> CRcarrier R) (l : CRcarrier R),
+    CR_cv R xn l
+    -> CR_cv R (fun n => - xn n) (- l).
+Proof.
+  intros. intro p. specialize (H p) as [n nmaj].
+  exists n. intros. specialize (nmaj i H).
+  apply (CRle_trans _ (CRabs R (CRminus R (xn i) l))).
+  2: exact nmaj. clear nmaj H.
+  unfold CRminus. rewrite <- CRopp_plus_distr, CRabs_opp.
+  apply CRle_refl.
+Qed.
+
+Lemma CR_cv_plus : forall {R : ConstructiveReals} (xn yn : nat -> CRcarrier R) (a b : CRcarrier R),
+    CR_cv R xn a
+    -> CR_cv R yn b
+    -> CR_cv R (fun n => xn n + yn n) (a + b).
+Proof.
+  intros. intro p.
+  specialize (H (2*p)%positive) as [i imaj].
+  specialize (H0 (2*p)%positive) as [j jmaj].
+  exists (max i j). intros.
+  apply (CRle_trans
+           _ (CRabs R (CRplus R (CRminus R (xn i0) a) (CRminus R (yn i0) b)))).
+  apply CRabs_morph.
+  - unfold CRminus.
+    do 2 rewrite <- (Radd_assoc (CRisRing R)).
+    apply CRplus_morph. reflexivity. rewrite CRopp_plus_distr.
+    destruct (CRisRing R). rewrite Radd_comm, <- Radd_assoc.
+    apply CRplus_morph. reflexivity.
+    rewrite Radd_comm. reflexivity.
+  - apply (CRle_trans _ _ _ (CRabs_triang _ _)).
+    apply (CRle_trans _ (CRplus R (CR_of_Q R (1 # 2*p)) (CR_of_Q R (1 # 2*p)))).
+    apply CRplus_le_compat. apply imaj, (le_trans _ _ _ (Nat.le_max_l _ _) H).
+    apply jmaj, (le_trans _ _ _ (Nat.le_max_r _ _) H).
+    apply (CRle_trans _ (CR_of_Q R ((1 # 2 * p) + (1 # 2 * p)))).
+    apply CR_of_Q_plus. apply CR_of_Q_le.
+    rewrite Qinv_plus_distr. setoid_replace (1 + 1 # 2 * p) with (1 # p).
+    apply Qle_refl. reflexivity.
+Qed.
+
+Lemma CR_cv_unique : forall {R : ConstructiveReals} (xn : nat -> CRcarrier R)
+                       (a b : CRcarrier R),
+    CR_cv R xn a
+    -> CR_cv R xn b
+    -> a == b.
+Proof.
+  intros. assert (CR_cv R (fun _ => CRzero R) (CRminus R b a)).
+  { apply (CR_cv_extens (fun n => CRminus R (xn n) (xn n))).
+    intro n. unfold CRminus. apply CRplus_opp_r.
+    apply CR_cv_plus. exact H0. apply CR_cv_opp, H. }
+  assert (forall q r : Q, 0 < q -> / q < r -> 1 < q * r)%Q.
+  { intros. apply (Qmult_lt_l _ _ q) in H3.
+    rewrite Qmult_inv_r in H3. exact H3. intro abs.
+    rewrite abs in H2. exact (Qlt_irrefl 0 H2). exact H2. }
+  clear H H0 xn. remember (CRminus R b a) as z.
+  assert (z == 0). split.
+  - intro abs. destruct (CR_Q_dense R _ _ abs) as [q [H0 H]].
+    destruct (Qarchimedean (/(-q))) as [p pmaj].
+    specialize (H1 p) as [n nmaj].
+    specialize (nmaj n (le_refl n)). apply nmaj.
+    apply (CRlt_trans _ (CR_of_Q R (-q))). apply CR_of_Q_lt.
+    apply H2 in pmaj.
+    apply (Qmult_lt_r _ _ (1#p)) in pmaj. 2: reflexivity.
+    rewrite Qmult_1_l, <- Qmult_assoc in pmaj.
+    setoid_replace ((Z.pos p # 1) * (1 # p))%Q with 1%Q in pmaj.
+    rewrite Qmult_1_r in pmaj. exact pmaj. unfold Qeq, Qnum, Qden; simpl.
+    do 2 rewrite Pos.mul_1_r. reflexivity.
+    apply (Qplus_lt_l _ _ q). ring_simplify.
+    apply (lt_CR_of_Q R q 0). apply (CRlt_le_trans _ (CRzero R) _ H).
+    apply CR_of_Q_zero.
+    apply (CRlt_le_trans _ (CRopp R z)).
+    apply (CRle_lt_trans _ (CRopp R (CR_of_Q R q))). apply CR_of_Q_opp.
+    apply CRopp_gt_lt_contravar, H0.
+    apply (CRle_trans _ (CRabs R (CRopp R z))).
+    pose proof (CRabs_def R (CRopp R z) (CRabs R (CRopp R z))) as [_ H1].
+    apply H1, CRle_refl.
+    apply CRabs_morph. unfold CRminus. symmetry. apply CRplus_0_l.
+  - intro abs. destruct (CR_Q_dense R _ _ abs) as [q [H0 H]].
+    destruct (Qarchimedean (/q)) as [p pmaj].
+    specialize (H1 p) as [n nmaj].
+    specialize (nmaj n (le_refl n)). apply nmaj.
+    apply (CRlt_trans _ (CR_of_Q R q)). apply CR_of_Q_lt.
+    apply H2 in pmaj.
+    apply (Qmult_lt_r _ _ (1#p)) in pmaj. 2: reflexivity.
+    rewrite Qmult_1_l, <- Qmult_assoc in pmaj.
+    setoid_replace ((Z.pos p # 1) * (1 # p))%Q with 1%Q in pmaj.
+    rewrite Qmult_1_r in pmaj. exact pmaj. unfold Qeq, Qnum, Qden; simpl.
+    do 2 rewrite Pos.mul_1_r. reflexivity.
+    apply (lt_CR_of_Q R 0 q). apply (CRle_lt_trans _ (CRzero R)).
+    2: exact H0. apply CR_of_Q_zero.
+    apply (CRlt_le_trans _ _ _ H).
+    apply (CRle_trans _ (CRabs R (CRopp R z))).
+    apply (CRle_trans _ (CRabs R z)).
+    pose proof (CRabs_def R z (CRabs R z)) as [_ H1].
+    apply H1. apply CRle_refl. apply CRabs_opp.
+    apply CRabs_morph. unfold CRminus. symmetry. apply CRplus_0_l.
+  - subst z. apply (CRplus_eq_reg_l (CRopp R a)).
+    apply (CReq_trans _ (CRzero R)). apply CRplus_opp_l.
+    destruct (CRisRing R).
+    apply (CReq_trans _ (CRplus R b (CRopp R a))). apply CReq_sym, H.
+    apply Radd_comm.
+Qed.
+
+Lemma CR_cv_eq : forall {R : ConstructiveReals}
+                   (v u : nat -> CRcarrier R) (s : CRcarrier R),
+    (forall n:nat, u n == v n)
+    -> CR_cv R u s
+    -> CR_cv R v s.
+Proof.
+  intros R v u s seq H1 p. specialize (H1 p) as [N H0].
+  exists N. intros. unfold CRminus. rewrite <- seq. apply H0, H.
+Qed.
+
+Lemma CR_cauchy_eq : forall {R : ConstructiveReals}
+                       (un vn : nat -> CRcarrier R),
+    (forall n:nat, un n == vn n)
+    -> CR_cauchy R un
+    -> CR_cauchy R vn.
+Proof.
+  intros. intro p. specialize (H0 p) as [n H0].
+  exists n. intros. specialize (H0 i j H1 H2).
+  unfold CRminus in H0. rewrite <- CRabs_def.
+  rewrite <- CRabs_def in H0.
+  do 2 rewrite H in H0. exact H0.
+Qed.
+
+Lemma CR_cv_proper : forall {R : ConstructiveReals}
+                       (un : nat -> CRcarrier R) (a b : CRcarrier R),
+    CR_cv R un a
+    -> a == b
+    -> CR_cv R un b.
+Proof.
+  intros. intro p. specialize (H p) as [n H].
+  exists n. intros. unfold CRminus. rewrite <- H0. apply H, H1.
+Qed.
+
+Instance CR_cv_morph
+  : forall {R : ConstructiveReals} (un : nat -> CRcarrier R), CMorphisms.Proper
+      (CMorphisms.respectful (CReq R) CRelationClasses.iffT) (CR_cv R un).
+Proof.
+  split. intros. apply (CR_cv_proper un x). exact H0. exact H.
+  intros. apply (CR_cv_proper un y). exact H0. symmetry. exact H.
+Qed.
+
+Lemma Un_cv_nat_real : forall {R : ConstructiveReals}
+                         (un : nat -> CRcarrier R) (l : CRcarrier R),
+    CR_cv R un l
+    -> forall eps : CRcarrier R,
+      0 < eps
+      -> { p : nat & forall i:nat, le p i -> CRabs R (un i - l) < eps }.
+Proof.
+  intros. destruct (CR_archimedean R (CRinv R eps (inr H0))) as [k kmaj].
+  assert (0 < CR_of_Q R (Z.pos k # 1)).
+  { rewrite <- CR_of_Q_zero. apply CR_of_Q_lt. reflexivity. }
+  specialize (H k) as [p pmaj].
+  exists p. intros.
+  apply (CRle_lt_trans _ (CR_of_Q R (1 # k))).
+  apply pmaj, H.
+  apply (CRmult_lt_reg_l (CR_of_Q R (Z.pos k # 1))). exact H1.
+  rewrite <- CR_of_Q_mult.
+  apply (CRle_lt_trans _ 1).
+  rewrite <- CR_of_Q_one. apply CR_of_Q_le.
+  unfold Qle; simpl. do 2 rewrite Pos.mul_1_r. apply Z.le_refl.
+  apply (CRmult_lt_reg_r (CRinv R eps (inr H0))).
+  apply CRinv_0_lt_compat, H0. rewrite CRmult_1_l, CRmult_assoc.
+  rewrite CRinv_r, CRmult_1_r. exact kmaj.
+Qed.
+
+Lemma Un_cv_real_nat : forall {R : ConstructiveReals}
+                         (un : nat -> CRcarrier R) (l : CRcarrier R),
+    (forall eps : CRcarrier R,
+      0 < eps
+      -> { p : nat & forall i:nat, le p i -> CRabs R (un i - l) < eps })
+    -> CR_cv R un l.
+Proof.
+  intros. intros n.
+  specialize (H (CR_of_Q R (1#n))) as [p pmaj].
+  rewrite <- CR_of_Q_zero. apply CR_of_Q_lt. reflexivity.
+  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),
+    CR_cv R An l1 -> CR_cv R Bn l2
+    -> CR_cv R (fun i:nat => An i - Bn i) (l1 - l2).
+Proof.
+  intros. apply CR_cv_plus. apply H.
+  intros p. specialize (H0 p) as [n H0]. exists n.
+  intros. setoid_replace (- Bn i - - l2) with (- (Bn i - l2)).
+  rewrite CRabs_opp. apply H0, H1. unfold CRminus.
+  rewrite CRopp_plus_distr, CRopp_involutive. reflexivity.
+Qed.
+
+Lemma CR_cv_nonneg :
+  forall {R : ConstructiveReals} (An:nat -> CRcarrier R) (l:CRcarrier R),
+    CR_cv R An l
+    -> (forall n:nat, 0 <= An n)
+    -> 0 <= l.
+Proof.
+  intros. intro abs.
+  destruct (Un_cv_nat_real _ l H (-l)) as [N H1].
+  rewrite <- CRopp_0. apply CRopp_gt_lt_contravar. apply abs.
+  specialize (H1 N (le_refl N)).
+  pose proof (CRabs_def R (An N - l) (CRabs R (An N - l))) as [_ H2].
+  apply (CRle_lt_trans _ _ _ (CRle_abs _)) in H1.
+  apply (H0 N). apply (CRplus_lt_reg_r (-l)).
+  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).
+Proof.
+  intros. intros n.
+  destruct (CR_archimedean R (1 + CRabs R a)).
+  destruct (H (n * x)%positive).
+  exists x0. intros.
+  unfold CRminus. rewrite CRopp_mult_distr_l.
+  rewrite <- CRmult_plus_distr_r.
+  apply (CRle_trans _ ((CR_of_Q R (1 # n * x)) * CRabs R a)).
+  rewrite CRabs_mult. apply CRmult_le_compat_r. apply CRabs_pos.
+  apply c0, H0.
+  setoid_replace (1 # n * x)%Q with ((1 # n) *(1# x))%Q. 2: reflexivity.
+  rewrite <- (CRmult_1_r (CR_of_Q R (1#n))).
+  rewrite CR_of_Q_mult, CRmult_assoc.
+  apply CRmult_le_compat_l. rewrite <- CR_of_Q_zero.
+  apply CR_of_Q_le. discriminate. intro abs.
+  apply (CRmult_lt_compat_l (CR_of_Q R (Z.pos x #1))) in abs.
+  rewrite CRmult_1_r, <- CRmult_assoc, <- CR_of_Q_mult in abs.
+  rewrite (CR_of_Q_morph R ((Z.pos x # 1) * (1 # x))%Q 1%Q) in abs.
+  rewrite CR_of_Q_one, CRmult_1_l in abs.
+  apply (CRlt_asym _ _ abs), (CRlt_trans _ (1 + CRabs R a)).
+  2: exact c. rewrite <- CRplus_0_l, <- CRplus_assoc.
+  apply CRplus_lt_compat_r. rewrite CRplus_0_r. apply CRzero_lt_one.
+  unfold Qmult, Qeq, Qnum, Qden. ring_simplify. rewrite Pos.mul_1_l.
+  reflexivity.
+  apply (CRlt_trans _ (1+CRabs R a)). 2: exact c.
+  rewrite CRplus_comm.
+  rewrite <- (CRplus_0_r 0). apply CRplus_le_lt_compat.
+  apply CRabs_pos. apply CRzero_lt_one.
+Qed.
+
+Lemma CR_cv_const : forall {R : ConstructiveReals} (a : CRcarrier R),
+    CR_cv R (fun n => a) a.
+Proof.
+  intros a p. exists O. intros.
+  unfold CRminus. rewrite CRplus_opp_r.
+  rewrite CRabs_right. rewrite <- CR_of_Q_zero.
+  apply CR_of_Q_le. discriminate. apply CRle_refl.
+Qed.
+
+Lemma Rcv_cauchy_mod : forall {R : ConstructiveReals}
+                         (un : nat -> CRcarrier R) (l : CRcarrier R),
+    CR_cv R un l -> CR_cauchy R un.
+Proof.
+  intros. intros p. specialize (H (2*p)%positive) as [k H].
+  exists k. intros n q H0 H1.
+  setoid_replace (1#p)%Q with ((1#2*p) + (1#2*p))%Q.
+  rewrite CR_of_Q_plus.
+  setoid_replace (un n - un q) with ((un n - l) - (un q - l)).
+  apply (CRle_trans _ _ _ (CRabs_triang _ _)).
+  apply CRplus_le_compat.
+  - apply H, H0.
+  - rewrite CRabs_opp. apply H. apply H1.
+  - unfold CRminus. rewrite CRplus_assoc. apply CRplus_morph.
+    reflexivity. rewrite CRplus_comm, CRopp_plus_distr, CRopp_involutive.
+    rewrite CRplus_assoc, CRplus_opp_r, CRplus_0_r. reflexivity.
+  - 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.
+Proof.
+  induction p.
+  - intros. inversion H0. apply CRle_refl.
+  - intros. apply Nat.le_succ_r in H0. destruct H0.
+    apply (CRle_trans _ (un p)). apply IHp, H0. apply H.
+    subst n. apply CRle_refl.
+Qed.
+
+Lemma growing_ineq :
+  forall {R : ConstructiveReals} (Un:nat -> CRcarrier R) (l:CRcarrier R),
+    (forall n:nat, Un n <= Un (S n))
+    -> CR_cv R Un l -> forall n:nat, Un n <= l.
+Proof.
+  intros. intro abs.
+  destruct (Un_cv_nat_real _ l H0 (Un n - l)) as [N H1].
+  rewrite <- (CRplus_opp_r l). apply CRplus_lt_compat_r. exact abs.
+  specialize (H1 (max n N) (Nat.le_max_r _ _)).
+  apply (CRle_lt_trans _ _ _ (CRle_abs _)) in H1.
+  apply CRplus_lt_reg_r in H1.
+  apply (CR_growing_transit Un H n (max n N)). apply Nat.le_max_l.
+  exact H1.
+Qed.
+
+Lemma CR_cv_open_below
+  : forall {R : ConstructiveReals}
+      (un : nat -> CRcarrier R) (m l : CRcarrier R),
+    CR_cv R un l
+    -> m < l
+    -> { n : nat & forall i:nat, le n i -> m < un i }.
+Proof.
+  intros. apply CRlt_minus in H0.
+  pose proof (Un_cv_nat_real _ l H (l-m) H0) as [n nmaj].
+  exists n. intros. specialize (nmaj i H1).
+  apply CRabs_lt in nmaj.
+  destruct nmaj as [_ nmaj]. unfold CRminus in nmaj.
+  rewrite CRopp_plus_distr, CRopp_involutive, CRplus_comm in nmaj.
+  apply CRplus_lt_reg_l in nmaj.
+  apply (CRplus_lt_reg_l R (-m)). rewrite CRplus_opp_l.
+  apply (CRplus_lt_reg_r (-un i)). rewrite CRplus_0_l.
+  rewrite CRplus_assoc, CRplus_opp_r, CRplus_0_r. exact nmaj.
+Qed.
+
+Lemma CR_cv_open_above
+  : forall {R : ConstructiveReals}
+      (un : nat -> CRcarrier R) (m l : CRcarrier R),
+    CR_cv R un l
+    -> l < m
+    -> { n : nat & forall i:nat, le n i -> un i < m }.
+Proof.
+  intros. apply CRlt_minus in H0.
+  pose proof (Un_cv_nat_real _ l H (m-l) H0) as [n nmaj].
+  exists n. intros. specialize (nmaj i H1).
+  apply CRabs_lt in nmaj.
+  destruct nmaj as [nmaj _]. apply CRplus_lt_reg_r in nmaj.
+  exact nmaj.
+Qed.
+
+Lemma CR_cv_bound_down : forall {R : ConstructiveReals}
+                           (u : nat -> CRcarrier R) (A l : CRcarrier R) (N : nat),
+    (forall n:nat, le N n -> A <= u n)
+    -> CR_cv R u l
+    -> A <= l.
+Proof.
+  intros. intro r.
+  apply (CRplus_lt_compat_r (-l)) in r. rewrite CRplus_opp_r in r.
+  destruct (Un_cv_nat_real _ l H0 (A - l) r) as [n H1].
+  apply (H (n+N)%nat).
+  rewrite <- (plus_0_l N). rewrite Nat.add_assoc.
+  apply Nat.add_le_mono_r. apply le_0_n.
+  specialize (H1 (n+N)%nat). apply (CRplus_lt_reg_r (-l)).
+  assert (n + N >= n)%nat. rewrite <- (plus_0_r n). rewrite <- plus_assoc.
+  apply Nat.add_le_mono_l. apply le_0_n. specialize (H1 H2).
+  apply (CRle_lt_trans _ (CRabs R (u (n + N)%nat - l))).
+  apply CRle_abs. assumption.
+Qed.
+
+Lemma CR_cv_bound_up : forall {R : ConstructiveReals}
+                         (u : nat -> CRcarrier R) (A l : CRcarrier R) (N : nat),
+    (forall n:nat, le N n -> u n <= A)
+    -> CR_cv R u l
+    -> l <= A.
+Proof.
+  intros. intro r.
+  apply (CRplus_lt_compat_r (-A)) in r. rewrite CRplus_opp_r in r.
+  destruct (Un_cv_nat_real _ l H0 (l-A) r) as [n H1].
+  apply (H (n+N)%nat).
+  - rewrite <- (plus_0_l N). apply Nat.add_le_mono_r. apply le_0_n.
+  - specialize (H1 (n+N)%nat). apply (CRplus_lt_reg_l R (l - A - u (n+N)%nat)).
+    unfold CRminus. repeat rewrite CRplus_assoc.
+    rewrite CRplus_opp_l, CRplus_0_r, (CRplus_comm (-A)).
+    rewrite CRplus_assoc, CRplus_opp_r, CRplus_0_r.
+    apply (CRle_lt_trans _ _ _ (CRle_abs _)).
+    fold (l - u (n+N)%nat). rewrite CRabs_minus_sym. apply H1.
+    rewrite <- (plus_0_r n). rewrite <- plus_assoc.
+    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)
+    -> CR_cv R u a
+    -> CR_cv R v b
+    -> a <= b.
+Proof.
+  intros. apply (CRplus_le_reg_r (-a)). rewrite CRplus_opp_r.
+  apply (CR_cv_bound_down (fun i:nat => v i - u i) _ _ 0).
+  intros. rewrite <- (CRplus_opp_l (u n)).
+  unfold CRminus.
+  rewrite (CRplus_comm (v n)). apply CRplus_le_compat_l.
+  apply H. apply CR_cv_plus. exact H1. apply CR_cv_opp, H0.
+Qed.
+
+Lemma CR_cv_abs_cont : forall {R : ConstructiveReals}
+                         (u : nat -> CRcarrier R) (s : CRcarrier R),
+    CR_cv R u s
+    -> CR_cv R (fun n => CRabs R (u n)) (CRabs R s).
+Proof.
+  intros. intros eps. specialize (H eps) as [N lim].
+  exists N. intros n H.
+  apply (CRle_trans _ (CRabs R (u n - s))). apply CRabs_triang_inv2.
+  apply lim. assumption.
+Qed.
+
+Lemma CR_cv_dist_cont : forall {R : ConstructiveReals}
+                          (u : nat -> CRcarrier R) (a s : CRcarrier R),
+    CR_cv R u s
+    -> CR_cv R (fun n => CRabs R (a - u n)) (CRabs R (a - s)).
+Proof.
+  intros. apply CR_cv_abs_cont.
+  intros eps. specialize (H eps) as [N lim].
+  exists N. intros n H.
+  setoid_replace (a - u n - (a - s)) with (s - (u n)).
+  specialize (lim n).
+  rewrite CRabs_minus_sym.
+  apply lim. assumption.
+  unfold CRminus. rewrite CRopp_plus_distr, CRopp_involutive.
+  rewrite (CRplus_comm a), (CRplus_comm s).
+  rewrite CRplus_assoc. apply CRplus_morph. reflexivity.
+  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, CR_of_Q_one.
+  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. rewrite CR_of_Q_zero.
+    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. rewrite CR_of_Q_one.
+    apply pow_R1_Rle. rewrite <- CR_of_Q_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 pow_le; rewrite <- CR_of_Q_zero; apply CR_of_Q_le; discriminate.
+  apply CRlt_asym.
+  apply (CRmult_lt_reg_l (CR_of_Q R (Z.pos p # 1))).
+  rewrite <- CR_of_Q_zero. apply CR_of_Q_lt. reflexivity. rewrite <- CR_of_Q_mult.
+  rewrite (CR_of_Q_morph R ((Z.pos p # 1) * (1 # p)) 1).
+  2: unfold Qmult, Qeq, Qnum, Qden; ring_simplify; reflexivity.
+  apply (CRmult_lt_reg_r (CRpow (CR_of_Q R 2) i)).
+  apply pow_lt. simpl. rewrite <- CR_of_Q_zero.
+  apply CR_of_Q_lt. reflexivity.
+  rewrite CRmult_assoc. rewrite pow_mult.
+  rewrite (pow_proper (CR_of_Q R (1 # 2) * CR_of_Q R 2) 1), pow_one.
+  rewrite CRmult_1_r, CR_of_Q_one, CRmult_1_l.
+  apply (CRle_lt_trans _ (INR i)). 2: exact (H i). clear H.
+  apply CR_of_Q_le. unfold Qle,Qnum,Qden.
+  do 2 rewrite Z.mul_1_r.
+  rewrite <- positive_nat_Z. apply Nat2Z.inj_le, H0.
+  rewrite <- CR_of_Q_mult. setoid_replace ((1#2)*2)%Q with 1%Q.
+  apply CR_of_Q_one. reflexivity.
+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_morph R _ (1+1)).
+    rewrite CR_of_Q_plus, CR_of_Q_one, CRplus_assoc.
+    rewrite CRplus_opp_r, CRplus_0_r. reflexivity. 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.
+    rewrite CR_of_Q_one. 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. rewrite <- CR_of_Q_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. rewrite CR_of_Q_zero.
+      apply CRzero_lt_one. apply (CRlt_le_trans _ (CRpow (CR_of_Q R 2) n + 1)).
+      unfold INR.
+      rewrite Nat2Z.inj_succ, <- Z.add_1_l.
+      rewrite (CR_of_Q_morph R _ (1 + (Z.of_nat n #1))).
+      2: symmetry; apply Qinv_plus_distr. rewrite CR_of_Q_plus.
+      rewrite CRplus_comm. rewrite CR_of_Q_one.
+      apply CRplus_lt_compat_r, IHn.
+      setoid_replace (CRpow (CR_of_Q R 2) (S n))
+        with (CRpow (CR_of_Q R 2) n + CRpow (CR_of_Q R 2) n).
+      apply CRplus_le_compat. apply CRle_refl.
+      apply pow_R1_Rle. rewrite <- CR_of_Q_one. apply CR_of_Q_le. discriminate.
+      rewrite <- CR_double. reflexivity. }
+    intros n. exists (Pos.to_nat n). intros.
+    setoid_replace (CR_of_Q R 2 - CRpow (CR_of_Q R (1 # 2)) i - CR_of_Q R 2)
+      with (- CRpow (CR_of_Q R (1 # 2)) i).
+    rewrite CRabs_opp. rewrite CRabs_right.
+    assert (0 < CR_of_Q R 2).
+    { rewrite <- CR_of_Q_zero. apply CR_of_Q_lt. reflexivity. }
+    rewrite (pow_proper _ (CRinv R (CR_of_Q R 2) (inr H1))).
+    rewrite pow_inv. apply CRlt_asym.
+    apply (CRmult_lt_reg_l (CRpow (CR_of_Q R 2) i)). apply pow_lt, H1.
+    rewrite CRinv_r.
+    apply (CRmult_lt_reg_r (CR_of_Q R (Z.pos n#1))).
+    rewrite <- CR_of_Q_zero. apply CR_of_Q_lt. reflexivity.
+    rewrite CRmult_1_l, CRmult_assoc.
+    rewrite <- CR_of_Q_mult.
+    rewrite (CR_of_Q_morph R ((1 # n) * (Z.pos n # 1)) 1). 2: reflexivity.
+    rewrite CR_of_Q_one, CRmult_1_r. apply (CRle_lt_trans _ (INR i)).
+    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.
+    apply CR_of_Q_one. reflexivity.
+    apply CRlt_asym, pow_lt. rewrite <- CR_of_Q_zero.
+    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.
+Proof.
+  intros. intros eps.
+  specialize (H eps) as [N Nmaj].
+  exists (N+k)%nat. intros n H.
+  destruct (Nat.le_exists_sub k n).
+  apply (le_trans _ (N + k)). 2: exact H.
+  apply (le_trans _ (0 + k)). apply le_refl.
+  rewrite <- Nat.add_le_mono_r. apply le_0_n.
+  destruct H0.
+  subst n. apply Nmaj. unfold ge in H.
+  rewrite <- Nat.add_le_mono_r in H. exact H.
+Qed.
+
+Lemma CR_cv_shift' :
+  forall {R : ConstructiveReals} f k l,
+    CR_cv R f l -> CR_cv R (fun n => f (n + k)%nat) l.
+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.
+    rewrite <- CR_of_Q_zero. apply CR_of_Q_le. discriminate. apply CRle_refl.
+Qed.
diff --git a/theories/Reals/Abstract/ConstructiveReals.v b/theories/Reals/Abstract/ConstructiveReals.v
new file mode 100644
index 0000000000..d91fd1183a
--- /dev/null
+++ b/theories/Reals/Abstract/ConstructiveReals.v
@@ -0,0 +1,1149 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+(************************************************************************)
+
+(** An interface for constructive and computable real numbers.
+    All of its instances are isomorphic (see file ConstructiveRealsMorphisms).
+    For example it is implemented by the Cauchy reals in file
+    ConstructivecauchyReals and also implemented by the sumbool-based
+    Dedekind reals defined by
+
+Structure R := {
+  (* The cuts are represented as propositional functions, rather than subsets,
+     as there are no subsets in type theory. *)
+  lower : Q -> Prop;
+  upper : Q -> Prop;
+  (* The cuts respect equality on Q. *)
+  lower_proper : Proper (Qeq ==> iff) lower;
+  upper_proper : Proper (Qeq ==> iff) upper;
+  (* The cuts are inhabited. *)
+  lower_bound : { q : Q | lower q };
+  upper_bound : { r : Q | upper r };
+  (* The lower cut is a lower set. *)
+  lower_lower : forall q r, q < r -> lower r -> lower q;
+  (* The lower cut is open. *)
+  lower_open : forall q, lower q -> exists r, q < r /\ lower r;
+  (* The upper cut is an upper set. *)
+  upper_upper : forall q r, q < r -> upper q -> upper r;
+  (* The upper cut is open. *)
+  upper_open : forall r, upper r -> exists q,  q < r /\ upper q;
+  (* The cuts are disjoint. *)
+  disjoint : forall q, ~ (lower q /\ upper q);
+  (* There is no gap between the cuts. *)
+  located : forall q r, q < r -> { lower q } + { upper r }
+}.
+
+  see github.com/andrejbauer/dedekind-reals for the Prop-based
+  version of those Dedekind reals (although Prop fails to make
+  them an instance of ConstructiveReals).
+
+  Any computation about constructive reals can be worked
+  in the fastest instance for it; we then transport the results
+  to all other instances by the isomorphisms. This way of working
+  is different from the usual interfaces, where we would rather
+  prove things abstractly, by quantifying universally on the instance.
+
+  The functions of ConstructiveReals do not have a direct impact
+  on performance, because algorithms will be extracted from instances,
+  and because fast ConstructiveReals morphisms should be coded
+  manually. However, since instances are forced to implement
+  those functions, it is probable that they will also use them
+  in their algorithms. So those functions hint at what we think
+  will yield fast and small extracted programs.
+
+  Constructive reals are setoids, which custom equality is defined as
+  x == y  iff  (x <= y /\ y <= x).
+  It is hard to quotient constructively to get the Leibniz equality
+  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. *)
+
+
+Require Import QArith Qabs Qround.
+
+Definition isLinearOrder {X : Set} (Xlt : X -> X -> Set) : Set
+  := (forall x y:X, Xlt x y -> Xlt y x -> False)
+     * (forall x y z : X, Xlt x y -> Xlt y z -> Xlt x z)
+     * (forall x y z : X, Xlt x z -> Xlt x y + Xlt y z).
+
+Structure ConstructiveReals : Type :=
+  {
+    CRcarrier : Set;
+
+    (* Put this order relation in sort Set rather than Prop,
+       to allow the definition of fast ConstructiveReals morphisms.
+       For example, the Cauchy reals do store information in
+       the proofs of CRlt, which is used in algorithms in sort Set. *)
+    CRlt : CRcarrier -> CRcarrier -> Set;
+    CRltLinear : isLinearOrder CRlt;
+
+    CRle (x y : CRcarrier) := CRlt y x -> False;
+    CReq (x y : CRcarrier) := CRle y x /\ CRle x y;
+    CRapart (x y : CRcarrier) := sum (CRlt x y) (CRlt y x);
+
+    (* The propositional truncation of CRlt. It facilitates proofs
+       when computations are not considered important, for example in
+       classical reals with extra logical axioms. *)
+    CRltProp : CRcarrier -> CRcarrier -> Prop;
+    (* This choice algorithm can be slow, keep it for the classical
+       quotient of the reals, where computations are blocked by
+       axioms like LPO. *)
+    CRltEpsilon : forall x y : CRcarrier, CRltProp x y -> CRlt x y;
+    CRltForget : forall x y : CRcarrier, CRlt x y -> CRltProp x y;
+    CRltDisjunctEpsilon : forall a b c d : CRcarrier,
+        (CRltProp a b \/ CRltProp c d) -> CRlt a b  +  CRlt c d;
+
+    (* Constants *)
+    CRzero : CRcarrier;
+    CRone : CRcarrier;
+
+    (* Addition and multiplication *)
+    CRplus : CRcarrier -> CRcarrier -> CRcarrier;
+    CRopp : CRcarrier -> CRcarrier; (* Computable opposite,
+                         stronger than Prop-existence of opposite *)
+    CRmult : CRcarrier -> CRcarrier -> CRcarrier;
+
+    CRisRing : ring_theory CRzero CRone CRplus CRmult
+                          (fun x y => CRplus x (CRopp y)) CRopp CReq;
+    CRisRingExt : ring_eq_ext CRplus CRmult CRopp CReq;
+
+    (* Compatibility with order *)
+    CRzero_lt_one : CRlt CRzero CRone; (* 0 # 1 would only allow 0 < 1 because
+                                    of Fmult_lt_0_compat so request 0 < 1 directly. *)
+    CRplus_lt_compat_l : forall r r1 r2 : CRcarrier,
+        CRlt r1 r2 -> CRlt (CRplus r r1) (CRplus r r2);
+    CRplus_lt_reg_l : forall r r1 r2 : CRcarrier,
+        CRlt (CRplus r r1) (CRplus r r2) -> CRlt r1 r2;
+    CRmult_lt_0_compat : forall x y : CRcarrier,
+        CRlt CRzero x -> CRlt CRzero y -> CRlt CRzero (CRmult x y);
+
+    (* A constructive total inverse function on F would need to be continuous,
+       which is impossible because we cannot connect plus and minus infinities.
+       Therefore it has to be a partial function, defined on non zero elements.
+       For this reason we cannot use Coq's field_theory and field tactic.
+
+       To implement Finv by Cauchy sequences we need orderAppart,
+       ~orderEq is not enough. *)
+    CRinv : forall x : CRcarrier, CRapart x CRzero -> CRcarrier;
+    CRinv_l : forall (r:CRcarrier) (rnz : CRapart r CRzero),
+        CReq (CRmult (CRinv r rnz) r) CRone;
+    CRinv_0_lt_compat : forall (r : CRcarrier) (rnz : CRapart r CRzero),
+        CRlt CRzero r -> CRlt CRzero (CRinv r rnz);
+
+    (* The initial field morphism (in characteristic zero).
+       The abstract definition by iteration of addition is
+       probably the slowest. Let each instance implement
+       a faster (and often simpler) version. *)
+    CR_of_Q : Q -> CRcarrier;
+    CR_of_Q_plus : forall q r : Q, CReq (CR_of_Q (q+r))
+                                           (CRplus (CR_of_Q q) (CR_of_Q r));
+    CR_of_Q_mult : forall q r : Q, CReq (CR_of_Q (q*r))
+                                           (CRmult (CR_of_Q q) (CR_of_Q r));
+    CR_of_Q_one : CReq (CR_of_Q 1) CRone;
+    CR_of_Q_lt : forall q r : Q,
+        Qlt q r -> CRlt (CR_of_Q q) (CR_of_Q r);
+    lt_CR_of_Q : forall q r : Q,
+        CRlt (CR_of_Q q) (CR_of_Q r) -> Qlt q r;
+
+    (* This function is very fast in both the Cauchy and Dedekind
+       instances, because this rational number q is almost what
+       the proof of CRlt x y contains.
+       This function is also the heart of the computation of
+       constructive real numbers : it approximates x to any
+       requested precision y. *)
+    CR_Q_dense : forall x y : CRcarrier, CRlt x y ->
+       { q : Q  &  prod (CRlt x (CR_of_Q q))
+                        (CRlt (CR_of_Q q) y) };
+    CR_archimedean : forall x : CRcarrier,
+        { n : positive  &  CRlt x (CR_of_Q (Z.pos n # 1)) };
+
+    CRminus (x y : CRcarrier) : CRcarrier
+    := CRplus x (CRopp y);
+
+    (* Absolute value, CRabs x is the least upper bound
+       of the pair x, -x. *)
+    CRabs : CRcarrier -> CRcarrier;
+    CRabs_def : forall x y : CRcarrier,
+        (CRle x y /\ CRle (CRopp x) y)
+        <-> CRle (CRabs x) y;
+
+    (* Definitions of convergence and Cauchy-ness. The formulas
+       with orderLe or CRlt are logically equivalent, the choice of
+       orderLe in sort Prop is a question of performance.
+       It is very rare to turn back to the strict order to
+       define functions in sort Set, so we prefer to discard
+       those proofs during extraction. And even in those rare cases,
+       it is easy to divide epsilon by 2 for example. *)
+    CR_cv (un : nat -> CRcarrier) (l : CRcarrier) : Set
+    := forall p:positive,
+        { n : nat  |  forall i:nat, le n i
+                           -> CRle (CRabs (CRminus (un i) l))
+                                  (CR_of_Q (1#p)) };
+    CR_cauchy (un : nat -> CRcarrier) : Set
+    := forall p : positive,
+        { n : nat  |  forall i j:nat, le n i -> le n j
+                             -> CRle (CRabs (CRminus (un i) (un j)))
+                                    (CR_of_Q (1#p)) };
+
+    (* For the Cauchy reals, this algorithm consists in building
+       a Cauchy sequence of rationals un : nat -> Q that has
+       the same limit as xn. For each n:nat, un n is a 1/n
+       rational approximation of a point of xn that has converged
+       within 1/n. *)
+    CR_complete :
+      forall xn : (nat -> CRcarrier),
+        CR_cauchy xn -> { l : CRcarrier  &  CR_cv xn l };
+  }.
+
+Declare Scope ConstructiveReals.
+
+Delimit Scope ConstructiveReals with ConstructiveReals.
+
+Notation "x < y" := (CRlt _ x y) : ConstructiveReals.
+Notation "x <= y" := (CRle _ x y) : ConstructiveReals.
+Notation "x <= y <= z" := (CRle _ x y /\ CRle _ y z) : ConstructiveReals.
+Notation "x < y < z"   := (prod (CRlt _ x y) (CRlt _ y z)) : ConstructiveReals.
+Notation "x == y" := (CReq _ x y) : ConstructiveReals.
+Notation "x ≶ y" := (CRapart _ x y) (at level 70, no associativity) : ConstructiveReals.
+Notation "0" := (CRzero _) : ConstructiveReals.
+Notation "1" := (CRone _) : ConstructiveReals.
+Notation "x + y" := (CRplus _ x y) : ConstructiveReals.
+Notation "- x" := (CRopp _ x) : ConstructiveReals.
+Notation "x - y" := (CRminus _ x y) : ConstructiveReals.
+Notation "x * y" := (CRmult _ x y) : ConstructiveReals.
+Notation "/ x" := (CRinv _ x)  : ConstructiveReals.
+
+Local Open Scope ConstructiveReals.
+
+Lemma CRlt_asym : forall {R : ConstructiveReals} (x y : CRcarrier R),
+    x < y -> x <= y.
+Proof.
+  intros. intro H0. destruct (CRltLinear R), p.
+  apply (f x y); assumption.
+Qed.
+
+Lemma CRlt_proper
+  : forall R : ConstructiveReals,
+    CMorphisms.Proper
+      (CMorphisms.respectful (CReq R)
+                             (CMorphisms.respectful (CReq R) CRelationClasses.iffT)) (CRlt R).
+Proof.
+  intros R x y H x0 y0 H0. destruct H, H0.
+  destruct (CRltLinear R). split.
+  - intro. destruct (s x y x0). assumption.
+    contradiction. destruct (s y y0 x0).
+    assumption. assumption. contradiction.
+  - intro. destruct (s y x y0). assumption.
+    contradiction. destruct (s x x0 y0).
+    assumption. assumption. contradiction.
+Qed.
+
+Lemma CRle_refl : forall {R : ConstructiveReals} (x : CRcarrier R),
+    x <= x.
+Proof.
+  intros. intro H. destruct (CRltLinear R), p.
+  exact (f x x H H).
+Qed.
+
+Lemma CRle_lt_trans : forall {R : ConstructiveReals} (r1 r2 r3 : CRcarrier R),
+    r1 <= r2 -> r2 < r3 -> r1 < r3.
+Proof.
+  intros. destruct (CRltLinear R).
+  destruct (s r2 r1 r3 H0). contradiction. apply c.
+Qed.
+
+Lemma CRlt_le_trans : forall {R : ConstructiveReals} (r1 r2 r3 : CRcarrier R),
+    r1 < r2 -> r2 <= r3 -> r1 < r3.
+Proof.
+  intros. destruct (CRltLinear R).
+  destruct (s r1 r3 r2 H). apply c. contradiction.
+Qed.
+
+Lemma CRle_trans : forall {R : ConstructiveReals} (x y z : CRcarrier R),
+    x <= y -> y <= z -> x <= z.
+Proof.
+  intros. intro abs. apply H0.
+  apply (CRlt_le_trans _ x); assumption.
+Qed.
+
+Lemma CRlt_trans : forall {R : ConstructiveReals} (x y z : CRcarrier R),
+    x < y -> y < z -> x < z.
+Proof.
+  intros. apply (CRlt_le_trans _ y _ H).
+  apply CRlt_asym. exact H0.
+Defined.
+
+Lemma CRlt_trans_flip : forall {R : ConstructiveReals} (x y z : CRcarrier R),
+    y < z -> x < y -> x < z.
+Proof.
+  intros. apply (CRlt_le_trans _ y). exact H0.
+  apply CRlt_asym. exact H.
+Defined.
+
+Lemma CReq_refl : forall {R : ConstructiveReals} (x : CRcarrier R),
+    x == x.
+Proof.
+  split; apply CRle_refl.
+Qed.
+
+Lemma CReq_sym : forall {R : ConstructiveReals} (x y : CRcarrier R),
+    x == y -> y == x.
+Proof.
+  intros. destruct H. split; intro abs; contradiction.
+Qed.
+
+Lemma CReq_trans : forall {R : ConstructiveReals} (x y z : CRcarrier R),
+    x == y -> y == z -> x == z.
+Proof.
+  intros. destruct H,H0. destruct (CRltLinear R), p. split.
+  - intro abs. destruct (s _ y _ abs); contradiction.
+  - intro abs. destruct (s _ y _ abs); contradiction.
+Qed.
+
+Add Parametric Relation {R : ConstructiveReals} : (CRcarrier R) (CReq R)
+    reflexivity proved by (CReq_refl)
+    symmetry proved by (CReq_sym)
+    transitivity proved by (CReq_trans)
+      as CReq_rel.
+
+Instance CReq_relT : forall {R : ConstructiveReals},
+    CRelationClasses.Equivalence (CReq R).
+Proof.
+  split. exact CReq_refl. exact CReq_sym. exact CReq_trans.
+Qed.
+
+Instance CRlt_morph
+  : forall {R : ConstructiveReals}, CMorphisms.Proper
+      (CMorphisms.respectful (CReq R) (CMorphisms.respectful (CReq R) CRelationClasses.iffT)) (CRlt R).
+Proof.
+  intros R x y H x0 y0 H0. destruct H, H0. split.
+  - intro. destruct (CRltLinear R). destruct (s x y x0). assumption.
+    contradiction. destruct (s y y0 x0).
+    assumption. assumption. contradiction.
+  - intro. destruct (CRltLinear R). destruct (s y x y0). assumption.
+    contradiction. destruct (s x x0 y0).
+    assumption. assumption. contradiction.
+Qed.
+
+Add Parametric Morphism {R : ConstructiveReals} : (CRle R)
+    with signature CReq R ==> CReq R ==> iff
+      as CRle_morph.
+Proof.
+  intros. split.
+  - intros H1 H2. unfold CRle in H1.
+    rewrite <- H0 in H2. rewrite <- H in H2. contradiction.
+  - intros H1 H2. unfold CRle in H1.
+    rewrite H0 in H2. rewrite H in H2. contradiction.
+Qed.
+
+Lemma CRplus_0_l : forall {R : ConstructiveReals} (x : CRcarrier R),
+    0 + x == x.
+Proof.
+  intros. destruct (CRisRing R). apply Radd_0_l.
+Qed.
+
+Lemma CRplus_0_r : forall {R : ConstructiveReals} (x : CRcarrier R),
+    x + 0 == x.
+Proof.
+  intros. destruct (CRisRing R).
+  transitivity (0 + x).
+  apply Radd_comm. apply Radd_0_l.
+Qed.
+
+Lemma CRplus_opp_l : forall {R : ConstructiveReals} (x : CRcarrier R),
+    - x + x == 0.
+Proof.
+  intros. destruct (CRisRing R).
+  transitivity (x + - x).
+  apply Radd_comm. apply Ropp_def.
+Qed.
+
+Lemma CRplus_opp_r : forall {R : ConstructiveReals} (x : CRcarrier R),
+    x + - x == 0.
+Proof.
+  intros. destruct (CRisRing R). apply Ropp_def.
+Qed.
+
+Lemma CRopp_0 : forall {R : ConstructiveReals},
+    CRopp R 0 == 0.
+Proof.
+  intros. rewrite <- CRplus_0_r, CRplus_opp_l.
+  reflexivity.
+Qed.
+
+Lemma CRplus_lt_compat_r : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R),
+    r1 < r2 -> r1 + r < r2 + r.
+Proof.
+  intros. destruct (CRisRing R).
+  apply (CRlt_proper R (CRplus R r r1) (CRplus R r1 r) (Radd_comm _ _)
+                     (CRplus R r2 r) (CRplus R r2 r)).
+  apply CReq_refl.
+  apply (CRlt_proper R _ _ (CReq_refl _) _ (CRplus R r r2)).
+  apply Radd_comm. apply CRplus_lt_compat_l. exact H.
+Qed.
+
+Lemma CRplus_lt_reg_r : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R),
+    r1 + r < r2 + r -> r1 < r2.
+Proof.
+  intros. destruct (CRisRing R).
+  apply (CRlt_proper R (CRplus R r r1) (CRplus R r1 r) (Radd_comm _ _)
+                     (CRplus R r2 r) (CRplus R r2 r)) in H.
+  2: apply CReq_refl.
+  apply (CRlt_proper R _ _ (CReq_refl _) _ (CRplus R r r2)) in H.
+  apply CRplus_lt_reg_l in H. exact H.
+  apply Radd_comm.
+Qed.
+
+Lemma CRplus_le_compat_l : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R),
+    r1 <= r2 -> r + r1 <= r + r2.
+Proof.
+  intros. intros abs. apply CRplus_lt_reg_l in abs. apply H. exact abs.
+Qed.
+
+Lemma CRplus_le_compat_r : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R),
+    r1 <= r2 -> r1 + r <= r2 + r.
+Proof.
+  intros. intros abs. apply CRplus_lt_reg_r in abs. apply H. exact abs.
+Qed.
+
+Lemma CRplus_le_compat : forall {R : ConstructiveReals} (r1 r2 r3 r4 : CRcarrier R),
+    r1 <= r2 -> r3 <= r4 -> r1 + r3 <= r2 + r4.
+Proof.
+  intros. apply (CRle_trans _ (CRplus R r2 r3)).
+  apply CRplus_le_compat_r, H. apply CRplus_le_compat_l, H0.
+Qed.
+
+Lemma CRle_minus : forall {R : ConstructiveReals} (x y : CRcarrier R),
+    x <= y -> 0 <= y - x.
+Proof.
+  intros. rewrite <- (CRplus_opp_r x).
+  apply CRplus_le_compat_r. exact H.
+Qed.
+
+Lemma CRplus_le_reg_l : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R),
+    r + r1 <= r + r2 -> r1 <= r2.
+Proof.
+  intros. intro abs. apply H. clear H.
+  apply CRplus_lt_compat_l. exact abs.
+Qed.
+
+Lemma CRplus_le_reg_r : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R),
+    r1 + r <= r2 + r -> r1 <= r2.
+Proof.
+  intros. intro abs. apply H. clear H.
+  apply CRplus_lt_compat_r. exact abs.
+Qed.
+
+Lemma CRplus_lt_le_compat :
+  forall {R : ConstructiveReals} (r1 r2 r3 r4 : CRcarrier R),
+    r1 < r2
+    -> r3 <= r4
+    -> r1 + r3 < r2 + r4.
+Proof.
+  intros. apply (CRlt_le_trans _ (CRplus R r2 r3)).
+  apply CRplus_lt_compat_r. exact H. intro abs.
+  apply CRplus_lt_reg_l in abs. contradiction.
+Qed.
+
+Lemma CRplus_le_lt_compat :
+  forall {R : ConstructiveReals} (r1 r2 r3 r4 : CRcarrier R),
+    r1 <= r2
+    -> r3 < r4
+    -> r1 + r3 < r2 + r4.
+Proof.
+  intros. apply (CRle_lt_trans _ (CRplus R r2 r3)).
+  apply CRplus_le_compat_r. exact H.
+  apply CRplus_lt_compat_l. exact H0.
+Qed.
+
+Lemma CRplus_eq_reg_l : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R),
+    r + r1 == r + r2 -> r1 == r2.
+Proof.
+  intros.
+  destruct (CRisRingExt R). clear Rmul_ext Ropp_ext.
+  pose proof (Radd_ext
+                (CRopp R r) (CRopp R r) (CReq_refl _)
+                _ _ H).
+  destruct (CRisRing R).
+  apply (CReq_trans r1) in H0.
+  apply (CReq_trans _ _ _ H0).
+  transitivity ((- r + r) + r2).
+  apply Radd_assoc. transitivity (0 + r2).
+  apply Radd_ext. apply CRplus_opp_l. apply CReq_refl.
+  apply Radd_0_l. apply CReq_sym.
+  transitivity (- r + r + r1).
+  apply Radd_assoc.
+  transitivity (0 + r1).
+  apply Radd_ext. apply CRplus_opp_l. apply CReq_refl.
+  apply Radd_0_l.
+Qed.
+
+Lemma CRplus_eq_reg_r : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R),
+    r1 + r == r2 + r -> r1 == r2.
+Proof.
+  intros. apply (CRplus_eq_reg_l r).
+  transitivity (r1 + r). apply (Radd_comm (CRisRing R)).
+  transitivity (r2 + r).
+  exact H. apply (Radd_comm (CRisRing R)).
+Qed.
+
+Lemma CRplus_assoc : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R),
+    r + r1 + r2 == r + (r1 + r2).
+Proof.
+  intros. symmetry. apply (Radd_assoc (CRisRing R)).
+Qed.
+
+Lemma CRplus_comm : forall {R : ConstructiveReals} (r1 r2 : CRcarrier R),
+    r1 + r2 == r2 + r1.
+Proof.
+  intros. apply (Radd_comm (CRisRing R)).
+Qed.
+
+Add Parametric Morphism {R : ConstructiveReals} : (CRplus R)
+    with signature CReq R ==> CReq R ==> CReq R
+      as CRplus_morph.
+Proof.
+  apply (CRisRingExt R).
+Qed.
+
+Add Parametric Morphism {R : ConstructiveReals} : (CRopp R)
+    with signature CReq R ==> CReq R
+      as CRopp_morph.
+Proof.
+  apply (CRisRingExt R).
+Qed.
+
+Add Parametric Morphism {R : ConstructiveReals} : (CRmult R)
+    with signature CReq R ==> CReq R ==> CReq R
+      as CRmult_morph.
+Proof.
+  apply (CRisRingExt R).
+Qed.
+
+Instance CRplus_morph_T
+  : forall {R : ConstructiveReals}, CMorphisms.Proper
+      (CMorphisms.respectful (CReq R) (CMorphisms.respectful (CReq R) (CReq R))) (CRplus R).
+Proof.
+  intros R x y H z t H1. apply CRplus_morph; assumption.
+Qed.
+
+Instance CRmult_morph_T
+  : forall {R : ConstructiveReals}, CMorphisms.Proper
+      (CMorphisms.respectful (CReq R) (CMorphisms.respectful (CReq R) (CReq R))) (CRmult R).
+Proof.
+  intros R x y H z t H1. apply CRmult_morph; assumption.
+Qed.
+
+Instance CRopp_morph_T
+  : forall {R : ConstructiveReals}, CMorphisms.Proper
+      (CMorphisms.respectful (CReq R) (CReq R)) (CRopp R).
+Proof.
+  apply CRisRingExt.
+Qed.
+
+Add Parametric Morphism {R : ConstructiveReals} : (CRminus R)
+    with signature (CReq R) ==> (CReq R) ==> (CReq R)
+      as CRminus_morph.
+Proof.
+  intros. unfold CRminus. rewrite H,H0. reflexivity.
+Qed.
+
+Instance CRminus_morph_T
+  : forall {R : ConstructiveReals}, CMorphisms.Proper
+      (CMorphisms.respectful (CReq R) (CMorphisms.respectful (CReq R) (CReq R))) (CRminus R).
+Proof.
+  intros R x y exy z t ezt. unfold CRminus. rewrite exy,ezt. reflexivity.
+Qed.
+
+Lemma CRopp_involutive : forall {R : ConstructiveReals} (r : CRcarrier R),
+    - - r == r.
+Proof.
+  intros. apply (CRplus_eq_reg_l (CRopp R r)).
+  transitivity (CRzero R). apply CRisRing.
+  apply CReq_sym. transitivity (r + - r).
+  apply CRisRing. apply CRisRing.
+Qed.
+
+Lemma CRopp_gt_lt_contravar
+  : forall {R : ConstructiveReals} (r1 r2 : CRcarrier R),
+    r2 < r1 -> - r1 < - r2.
+Proof.
+  intros. apply (CRplus_lt_reg_l R r1).
+  destruct (CRisRing R).
+  apply (CRle_lt_trans _ (CRzero R)). apply Ropp_def.
+  apply (CRplus_lt_compat_l R (CRopp R r2)) in H.
+  apply (CRle_lt_trans _ (CRplus R (CRopp R r2) r2)).
+  apply (CRle_trans _ (CRplus R r2 (CRopp R r2))).
+  destruct (Ropp_def r2). exact H0.
+  destruct (Radd_comm r2 (CRopp R r2)). exact H1.
+  apply (CRlt_le_trans _ _ _ H).
+  destruct (Radd_comm r1 (CRopp R r2)). exact H0.
+Qed.
+
+Lemma CRopp_lt_cancel : forall {R : ConstructiveReals} (r1 r2 : CRcarrier R),
+    - r2 < - r1 -> r1 < r2.
+Proof.
+  intros. apply (CRplus_lt_compat_r r1) in H.
+  rewrite (CRplus_opp_l r1) in H.
+  apply (CRplus_lt_compat_l R r2) in H.
+  rewrite CRplus_0_r, (Radd_assoc (CRisRing R)) in H.
+  rewrite CRplus_opp_r, (Radd_0_l (CRisRing R)) in H.
+  exact H.
+Qed.
+
+Lemma CRopp_ge_le_contravar
+  : forall {R : ConstructiveReals} (r1 r2 : CRcarrier R),
+    r2 <= r1 -> - r1 <= - r2.
+Proof.
+  intros. intros abs. apply CRopp_lt_cancel in abs. contradiction.
+Qed.
+
+Lemma CRopp_plus_distr : forall {R : ConstructiveReals} (r1 r2 : CRcarrier R),
+    - (r1 + r2) == - r1 + - r2.
+Proof.
+  intros. destruct (CRisRing R), (CRisRingExt R).
+  apply (CRplus_eq_reg_l (CRplus R r1 r2)).
+  transitivity (CRzero R). apply Ropp_def.
+  transitivity (r2 + r1 + (-r1 + -r2)).
+  transitivity (r2 + (r1 + (-r1 + -r2))).
+  transitivity (r2 + - r2).
+  apply CReq_sym. apply Ropp_def. apply Radd_ext.
+  apply CReq_refl.
+  transitivity (CRzero R + - r2).
+  apply CReq_sym, Radd_0_l.
+  transitivity (r1 + - r1 + - r2).
+  apply Radd_ext. 2: apply CReq_refl. apply CReq_sym, Ropp_def.
+  apply CReq_sym, Radd_assoc. apply Radd_assoc.
+  apply Radd_ext. 2: apply CReq_refl. apply Radd_comm.
+Qed.
+
+Lemma CRmult_1_l : forall {R : ConstructiveReals} (r : CRcarrier R),
+    1 * r == r.
+Proof.
+  intros. destruct (CRisRing R). apply Rmul_1_l.
+Qed.
+
+Lemma CRmult_1_r : forall {R : ConstructiveReals} (x : CRcarrier R),
+    x * 1 == x.
+Proof.
+  intros. destruct (CRisRing R). transitivity (CRmult R 1 x).
+  apply Rmul_comm. apply Rmul_1_l.
+Qed.
+
+Lemma CRmult_assoc : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R),
+    r * r1 * r2 == r * (r1 * r2).
+Proof.
+  intros. symmetry. apply (Rmul_assoc (CRisRing R)).
+Qed.
+
+Lemma CRmult_comm : forall {R : ConstructiveReals} (r s : CRcarrier R),
+    r * s == s * r.
+Proof.
+  intros. rewrite (Rmul_comm (CRisRing R) r). reflexivity.
+Qed.
+
+Lemma CRmult_plus_distr_l : forall {R : ConstructiveReals} (r1 r2 r3 : CRcarrier R),
+    r1 * (r2 + r3) == (r1 * r2) + (r1 * r3).
+Proof.
+  intros. destruct (CRisRing R).
+  transitivity ((r2 + r3) * r1).
+  apply Rmul_comm.
+  transitivity ((r2 * r1) + (r3 * r1)).
+  apply Rdistr_l.
+  transitivity ((r1 * r2) + (r3 * r1)).
+  destruct (CRisRingExt R). apply Radd_ext.
+  apply Rmul_comm. apply CReq_refl.
+  destruct (CRisRingExt R). apply Radd_ext.
+  apply CReq_refl. apply Rmul_comm.
+Qed.
+
+Lemma CRmult_plus_distr_r : forall {R : ConstructiveReals} (r1 r2 r3 : CRcarrier R),
+    (r2 + r3) * r1 == (r2 * r1) + (r3 * r1).
+Proof.
+  intros. do 3 rewrite <- (CRmult_comm r1).
+  apply CRmult_plus_distr_l.
+Qed.
+
+(* x == x+x -> x == 0 *)
+Lemma CRzero_double : forall {R : ConstructiveReals} (x : CRcarrier R),
+    x == x + x -> x == 0.
+Proof.
+  intros.
+  apply (CRplus_eq_reg_l x), CReq_sym. transitivity x.
+  apply CRplus_0_r. exact H.
+Qed.
+
+Lemma CRmult_0_r : forall {R : ConstructiveReals} (x : CRcarrier R),
+    x * 0 == 0.
+Proof.
+  intros. apply CRzero_double.
+  transitivity (x * (0 + 0)).
+  destruct (CRisRingExt R). apply Rmul_ext. apply CReq_refl.
+  apply CReq_sym, CRplus_0_r.
+  destruct (CRisRing R). apply CRmult_plus_distr_l.
+Qed.
+
+Lemma CRmult_0_l : forall {R : ConstructiveReals} (r : CRcarrier R),
+    0 * r == 0.
+Proof.
+  intros. rewrite CRmult_comm. apply CRmult_0_r.
+Qed.
+
+Lemma CRopp_mult_distr_r : forall {R : ConstructiveReals} (r1 r2 : CRcarrier R),
+    - (r1 * r2) == r1 * (- r2).
+Proof.
+  intros. apply (CRplus_eq_reg_l (CRmult R r1 r2)).
+  destruct (CRisRing R). transitivity (CRzero R). apply Ropp_def.
+  transitivity (r1 * (r2 + - r2)).
+  2: apply CRmult_plus_distr_l.
+  transitivity (r1 * 0).
+  apply CReq_sym, CRmult_0_r.
+  destruct (CRisRingExt R). apply Rmul_ext. apply CReq_refl.
+  apply CReq_sym, Ropp_def.
+Qed.
+
+Lemma CRopp_mult_distr_l : forall {R : ConstructiveReals} (r1 r2 : CRcarrier R),
+    - (r1 * r2) == (- r1) * r2.
+Proof.
+  intros. transitivity (r2 * - r1).
+  transitivity (- (r2 * r1)).
+  apply (Ropp_ext (CRisRingExt R)).
+  apply CReq_sym, (Rmul_comm (CRisRing R)).
+  apply CRopp_mult_distr_r.
+  apply CReq_sym, (Rmul_comm (CRisRing R)).
+Qed.
+
+Lemma CRmult_lt_compat_r : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R),
+    0 < r -> r1 < r2 -> r1 * r < r2 * r.
+Proof.
+  intros. apply (CRplus_lt_reg_r (CRopp R (CRmult R r1 r))).
+  apply (CRle_lt_trans _ (CRzero R)).
+  apply (Ropp_def (CRisRing R)).
+  apply (CRlt_le_trans _ (CRplus R (CRmult R r2 r) (CRmult R (CRopp R r1) r))).
+  apply (CRlt_le_trans _ (CRmult R (CRplus R r2 (CRopp R r1)) r)).
+  apply CRmult_lt_0_compat. 2: exact H.
+  apply (CRplus_lt_reg_r r1).
+  apply (CRle_lt_trans _ r1). apply (Radd_0_l (CRisRing R)).
+  apply (CRlt_le_trans _ r2 _ H0).
+  apply (CRle_trans _ (CRplus R r2 (CRplus R (CRopp R r1) r1))).
+  apply (CRle_trans _ (CRplus R r2 (CRzero R))).
+  destruct (CRplus_0_r r2). exact H1.
+  apply CRplus_le_compat_l. destruct (CRplus_opp_l r1). exact H1.
+  destruct (Radd_assoc (CRisRing R) r2 (CRopp R r1) r1). exact H2.
+  destruct (CRisRing R).
+  destruct (Rdistr_l r2 (CRopp R r1) r). exact H2.
+  apply CRplus_le_compat_l. destruct (CRopp_mult_distr_l r1 r).
+  exact H1.
+Qed.
+
+Lemma CRmult_lt_compat_l : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R),
+    0 < r -> r1 < r2 -> r * r1 < r * r2.
+Proof.
+  intros. do 2 rewrite (CRmult_comm r).
+  apply CRmult_lt_compat_r; assumption.
+Qed.
+
+Lemma CRinv_r : forall {R : ConstructiveReals} (r:CRcarrier R)
+                  (rnz : r ≶ (CRzero R)),
+    r * (/ r) rnz == 1.
+Proof.
+  intros. transitivity ((/ r) rnz * r).
+  apply (CRisRing R). apply CRinv_l.
+Qed.
+
+Lemma CRmult_lt_reg_r : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R),
+    0 < r -> r1 * r < r2 * r -> r1 < r2.
+Proof.
+  intros. apply (CRmult_lt_compat_r ((/ r) (inr H))) in H0.
+  2: apply CRinv_0_lt_compat, H.
+  apply (CRle_lt_trans _ ((r1 * r) * ((/ r) (inr H)))).
+  - clear H0. apply (CRle_trans _ (CRmult R r1 (CRone R))).
+    destruct (CRmult_1_r r1). exact H0.
+    apply (CRle_trans _ (CRmult R r1 (CRmult R r ((/ r) (inr H))))).
+    destruct (Rmul_ext (CRisRingExt R) r1 r1 (CReq_refl r1)
+                       (r * ((/ r) (inr H))) 1).
+    apply CRinv_r. exact H0.
+    destruct (Rmul_assoc (CRisRing R) r1 r ((/ r) (inr H))). exact H1.
+  - apply (CRlt_le_trans _ ((r2 * r) * ((/ r) (inr H)))).
+    exact H0. clear H0.
+    apply (CRle_trans _ (r2 * 1)).
+    2: destruct (CRmult_1_r r2); exact H1.
+    apply (CRle_trans _ (r2 * (r * ((/ r) (inr H))))).
+    destruct (Rmul_assoc (CRisRing R) r2 r ((/ r) (inr H))). exact H0.
+    destruct (Rmul_ext (CRisRingExt R) r2 r2 (CReq_refl r2)
+                       (r * ((/ r) (inr H))) (CRone R)).
+    apply CRinv_r. exact H1.
+Qed.
+
+Lemma CRmult_lt_reg_l : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R),
+    0 < r -> r * r1 < r * r2 -> r1 < r2.
+Proof.
+  intros.
+  rewrite (Rmul_comm (CRisRing R) r r1) in H0.
+  rewrite (Rmul_comm (CRisRing R) r r2) in H0.
+  apply CRmult_lt_reg_r in H0.
+  exact H0. exact H.
+Qed.
+
+Lemma CRmult_le_compat_l_half : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R),
+    0 < r -> r1 <= r2 -> r * r1 <= r * r2.
+Proof.
+  intros. intro abs. apply CRmult_lt_reg_l in abs.
+  contradiction. exact H.
+Qed.
+
+Lemma CRmult_le_compat_r_half : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R),
+    0 < r
+    -> r1 <= r2
+    -> r1 * r <= r2 * r.
+Proof.
+  intros. intro abs. apply CRmult_lt_reg_r in abs.
+  contradiction. exact H.
+Qed.
+
+Lemma CRmult_eq_reg_r : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R),
+    0 ≶ r
+    -> r1 * r == r2 * r
+    -> r1 == r2.
+Proof.
+  intros. destruct H0,H.
+  - split.
+    + intro abs. apply H0. apply CRmult_lt_compat_r.
+      exact c. exact abs.
+    + intro abs. apply H1. apply CRmult_lt_compat_r.
+      exact c. exact abs.
+  - split.
+    + intro abs. apply H1. apply CRopp_lt_cancel.
+      apply (CRle_lt_trans _ (CRmult R r1 (CRopp R r))).
+      apply CRopp_mult_distr_r.
+      apply (CRlt_le_trans _ (CRmult R r2 (CRopp R r))).
+      2: apply CRopp_mult_distr_r.
+      apply CRmult_lt_compat_r. 2: exact abs.
+      apply (CRplus_lt_reg_r r). apply (CRle_lt_trans _ r).
+      apply (Radd_0_l (CRisRing R)).
+      apply (CRlt_le_trans _ (CRzero R) _ c).
+      apply CRplus_opp_l.
+    + intro abs. apply H0. apply CRopp_lt_cancel.
+      apply (CRle_lt_trans _ (CRmult R r2 (CRopp R r))).
+      apply CRopp_mult_distr_r.
+      apply (CRlt_le_trans _ (CRmult R r1 (CRopp R r))).
+      2: apply CRopp_mult_distr_r.
+      apply CRmult_lt_compat_r. 2: exact abs.
+      apply (CRplus_lt_reg_r r). apply (CRle_lt_trans _ r).
+      apply (Radd_0_l (CRisRing R)).
+      apply (CRlt_le_trans _ (CRzero R) _ c).
+      apply CRplus_opp_l.
+Qed.
+
+Lemma CRinv_1 : forall {R : ConstructiveReals} (onz : CRapart R 1 0),
+    (/ 1) onz == 1.
+Proof.
+  intros. rewrite <- (CRmult_1_r ((/ 1) onz)).
+  rewrite CRinv_l. reflexivity.
+Qed.
+
+Lemma CRmult_eq_reg_l : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R),
+    r ≶ 0
+    -> r * r1 == r * r2
+    -> r1 == r2.
+Proof.
+  intros. rewrite (Rmul_comm (CRisRing R)) in H0.
+  rewrite (Rmul_comm (CRisRing R) r) in H0.
+  apply CRmult_eq_reg_r in H0. exact H0. destruct H.
+  right. exact c. left. exact c.
+Qed.
+
+Lemma CRinv_mult_distr :
+  forall {R : ConstructiveReals} (r1 r2 : CRcarrier R)
+    (r1nz : r1 ≶ 0) (r2nz : r2 ≶ 0)
+    (rmnz : (r1*r2) ≶ 0),
+    (/ (r1 * r2)) rmnz == (/ r1) r1nz * (/ r2) r2nz.
+Proof.
+  intros. apply (CRmult_eq_reg_l r1). exact r1nz.
+  rewrite (Rmul_assoc (CRisRing R)). rewrite CRinv_r. rewrite CRmult_1_l.
+  apply (CRmult_eq_reg_l r2). exact r2nz.
+  rewrite CRinv_r. rewrite (Rmul_assoc (CRisRing R)).
+  rewrite (CRmult_comm r2 r1). rewrite CRinv_r. reflexivity.
+Qed.
+
+Lemma CRinv_morph : forall {R : ConstructiveReals} (x y : CRcarrier R)
+                      (rxnz : x ≶ 0) (rynz : y ≶ 0),
+    x == y
+    -> (/ x) rxnz == (/ y) rynz.
+Proof.
+  intros. apply (CRmult_eq_reg_l x). exact rxnz.
+ rewrite CRinv_r, H, CRinv_r. reflexivity.
+Qed.
+
+Lemma CRlt_minus : forall {R : ConstructiveReals} (x y : CRcarrier R),
+    x < y -> 0 < y - x.
+Proof.
+  intros. rewrite <- (CRplus_opp_r x).
+  apply CRplus_lt_compat_r. exact H.
+Qed.
+
+Lemma CR_of_Q_le : forall {R : ConstructiveReals} (r q : Q),
+    Qle r q
+    -> CR_of_Q R r <= CR_of_Q R q.
+Proof.
+  intros. intro abs. apply lt_CR_of_Q in abs.
+  exact (Qlt_not_le _ _ abs H).
+Qed.
+
+Add Parametric Morphism {R : ConstructiveReals} : (CR_of_Q R)
+    with signature Qeq ==> CReq R
+      as CR_of_Q_morph.
+Proof.
+  split; apply CR_of_Q_le; rewrite H; apply Qle_refl.
+Qed.
+
+Lemma eq_inject_Q : forall {R : ConstructiveReals} (q r : Q),
+    CR_of_Q R q == CR_of_Q R r -> Qeq q r.
+Proof.
+  intros. destruct H. destruct (Q_dec q r). destruct s.
+  exfalso. apply (CR_of_Q_lt R q r) in q0. contradiction.
+  exfalso. apply (CR_of_Q_lt R r q) in q0. contradiction. exact q0.
+Qed.
+
+Instance CR_of_Q_morph_T
+  : forall {R : ConstructiveReals}, CMorphisms.Proper
+      (CMorphisms.respectful Qeq (CReq R)) (CR_of_Q R).
+Proof.
+  intros R x y H. apply CR_of_Q_morph; assumption.
+Qed.
+
+Lemma CR_of_Q_zero : forall {R : ConstructiveReals},
+    CR_of_Q R 0 == 0.
+Proof.
+  intros. apply CRzero_double.
+  transitivity (CR_of_Q R (0+0)). apply CR_of_Q_morph.
+  reflexivity. apply CR_of_Q_plus.
+Qed.
+
+Lemma CR_of_Q_opp : forall {R : ConstructiveReals} (q : Q),
+    CR_of_Q R (-q) == - CR_of_Q R q.
+Proof.
+  intros. apply (CRplus_eq_reg_l (CR_of_Q R q)).
+  transitivity (CRzero R).
+  transitivity (CR_of_Q R (q-q)).
+  apply CReq_sym, CR_of_Q_plus.
+  transitivity (CR_of_Q R 0).
+  apply CR_of_Q_morph. ring. apply CR_of_Q_zero.
+  apply CReq_sym. apply (CRisRing R).
+Qed.
+
+Lemma CR_of_Q_pos : forall {R : ConstructiveReals} (q:Q),
+    Qlt 0 q -> 0 < CR_of_Q R q.
+Proof.
+  intros. apply (CRle_lt_trans _ (CR_of_Q R 0)).
+  apply CR_of_Q_zero. apply CR_of_Q_lt. exact H.
+Qed.
+
+Lemma CR_of_Q_inv : forall {R : ConstructiveReals} (q : Q) (qPos : Qlt 0 q),
+    CR_of_Q R (/q)
+    == (/ CR_of_Q R q) (inr (CR_of_Q_pos q qPos)).
+Proof.
+  intros.
+  apply (CRmult_eq_reg_l (CR_of_Q R q)).
+  right. apply CR_of_Q_pos, qPos.
+  rewrite CRinv_r, <- CR_of_Q_mult, <- CR_of_Q_one.
+  apply CR_of_Q_morph. field. intro abs.
+  rewrite abs in qPos. exact (Qlt_irrefl 0 qPos).
+Qed.
+
+Lemma CRmult_le_0_compat : forall {R : ConstructiveReals} (a b : CRcarrier R),
+    0 <= a -> 0 <= b -> 0 <= a * b.
+Proof.
+  (* Limit of (a + 1/n)*b when n -> infty. *)
+  intros. intro abs.
+  assert (0 < -(a*b)) as epsPos.
+  { rewrite <- CRopp_0. apply CRopp_gt_lt_contravar. exact abs. }
+  destruct (CR_archimedean R (b * ((/ -(a*b)) (inr epsPos))))
+    as [n maj].
+  assert (0 < CR_of_Q R (Z.pos n #1)) as nPos.
+  { rewrite <- CR_of_Q_zero. apply CR_of_Q_lt. reflexivity. }
+  assert (b * (/ CR_of_Q R (Z.pos n #1)) (inr nPos) < -(a*b)).
+  { apply (CRmult_lt_reg_r (CR_of_Q R (Z.pos n #1))). apply nPos.
+    rewrite <- (Rmul_assoc (CRisRing R)), CRinv_l, CRmult_1_r.
+    apply (CRmult_lt_compat_r (-(a*b))) in maj.
+    rewrite CRmult_assoc, CRinv_l, CRmult_1_r in maj.
+    rewrite CRmult_comm. apply maj. apply epsPos. }
+  pose proof (CRmult_le_compat_l_half
+                (a + (/ CR_of_Q R (Z.pos n #1)) (inr nPos)) 0 b).
+  assert (0 + 0 < a + (/ CR_of_Q R (Z.pos n #1)) (inr nPos)).
+  { apply CRplus_le_lt_compat. apply H. apply CRinv_0_lt_compat. apply nPos. }
+  rewrite CRplus_0_l in H3. specialize (H2 H3 H0).
+  clear H3. rewrite CRmult_0_r in H2.
+  apply H2. clear H2. rewrite (Rdistr_l (CRisRing R)).
+  apply (CRplus_lt_compat_l R (a*b)) in H1.
+  rewrite CRplus_opp_r in H1.
+  rewrite (CRmult_comm ((/ CR_of_Q R (Z.pos n # 1)) (inr nPos))).
+  apply H1.
+Qed.
+
+Lemma CRmult_le_compat_l : forall {R : ConstructiveReals} (r r1 r2:CRcarrier R),
+    0 <= r -> r1 <= r2 -> r * r1 <= r * r2.
+Proof.
+  intros. apply (CRplus_le_reg_r (-(r*r1))).
+  rewrite CRplus_opp_r, CRopp_mult_distr_r.
+  rewrite <- CRmult_plus_distr_l.
+  apply CRmult_le_0_compat. exact H.
+  apply (CRplus_le_reg_r r1).
+  rewrite CRplus_0_l, CRplus_assoc, CRplus_opp_l, CRplus_0_r.
+  exact H0.
+Qed.
+
+Lemma CRmult_le_compat_r : forall {R : ConstructiveReals} (r r1 r2:CRcarrier R),
+    0 <= r -> r1 <= r2 -> r1 * r <= r2 * r.
+Proof.
+  intros. do 2 rewrite <- (CRmult_comm r).
+  apply CRmult_le_compat_l; assumption.
+Qed.
+
+Lemma CRmult_pos_pos
+  : forall {R : ConstructiveReals} (x y : CRcarrier R),
+    0 < x * y -> 0 <= x
+    -> 0 <= y -> 0 < x.
+Proof.
+  intros. destruct (CRltLinear R). clear p.
+  specialize (s 0 x 1 (CRzero_lt_one R)) as [H2|H2].
+  exact H2. apply CRlt_asym in H2.
+  apply (CRmult_le_compat_r y) in H2.
+  2: exact H1. rewrite CRmult_1_l in H2.
+  apply (CRlt_le_trans _ _ _ H) in H2.
+  rewrite <- (CRmult_0_l y) in H.
+  apply CRmult_lt_reg_r in H. exact H. exact H2.
+Qed.
+
+(* In particular x * y == 1 implies that 0 # x, 0 # y and
+   that x and y are inverses of each other. *)
+Lemma CRmult_pos_appart_zero
+  : forall {R : ConstructiveReals} (x y : CRcarrier R),
+    0 < x * y -> 0 ≶ x.
+Proof.
+  intros.
+  (* Narrow cases to x < 1. *)
+  destruct (CRltLinear R). clear p.
+  pose proof (s 0 x 1 (CRzero_lt_one R)) as [H0|H0].
+  left. exact H0.
+  (* In this case, linear order 0 y (x*y) decides. *)
+  destruct (s 0 y (x*y) H).
+  - left. rewrite <- (CRmult_0_l y) in H. apply CRmult_lt_reg_r in H.
+    exact H. exact c.
+  - right. apply CRopp_lt_cancel. rewrite CRopp_0.
+    apply (CRmult_pos_pos (-x) (-y)).
+    + rewrite <- CRopp_mult_distr_l, CRopp_mult_distr_r, CRopp_involutive. exact H.
+    + rewrite <- CRopp_0. apply CRopp_ge_le_contravar.
+      intro abs. rewrite <- (CRmult_0_r x) in H.
+      apply CRmult_lt_reg_l in H. rewrite <- (CRmult_1_l y) in c.
+      rewrite <- CRmult_assoc in c. apply CRmult_lt_reg_r in c.
+      rewrite CRmult_1_r in c. exact (CRlt_asym _ _ H0 c).
+      exact H. exact abs.
+    + intro abs. apply (CRmult_lt_compat_r y) in H0.
+      rewrite CRmult_1_l in H0. exact (CRlt_asym _ _ H0 c).
+      apply CRopp_lt_cancel. rewrite CRopp_0. exact abs.
+Qed.
+
+Lemma CRmult_le_reg_l :
+  forall {R : ConstructiveReals} (x y z : CRcarrier R),
+    0 < x -> x * y <= x * z -> y <= z.
+Proof.
+  intros. intro abs.
+  apply (CRmult_lt_compat_l x) in abs. contradiction.
+  exact H.
+Qed.
+
+Lemma CRmult_le_reg_r :
+  forall {R : ConstructiveReals} (x y z : CRcarrier R),
+    0 < x -> y * x <= z * x -> y <= z.
+Proof.
+  intros. intro abs.
+  apply (CRmult_lt_compat_r x) in abs. contradiction. exact H.
+Qed.
+
+Definition CRup_nat {R : ConstructiveReals} (x : CRcarrier R)
+  : { n : nat  &  x < CR_of_Q R (Z.of_nat n #1) }.
+Proof.
+  destruct (CR_archimedean R x). exists (Pos.to_nat x0).
+  rewrite positive_nat_Z. exact c.
+Qed.
+
+Definition CRfloor {R : ConstructiveReals} (a : CRcarrier R)
+  : { p : Z  &  prod (CR_of_Q R (p#1) < a)
+                     (a < CR_of_Q R (p#1) + CR_of_Q R 2) }.
+Proof.
+  destruct (CR_Q_dense R (a - CR_of_Q R (1#2)) a) as [q qmaj].
+  - apply (CRlt_le_trans _ (a-0)). apply CRplus_lt_compat_l.
+    apply CRopp_gt_lt_contravar. rewrite <- CR_of_Q_zero.
+    apply CR_of_Q_lt. reflexivity.
+    unfold CRminus. rewrite CRopp_0, CRplus_0_r. apply CRle_refl.
+  - exists (Qfloor q). destruct qmaj. split.
+    apply (CRle_lt_trans _ (CR_of_Q R q)). 2: exact c0.
+    apply CR_of_Q_le. apply Qfloor_le.
+    apply (CRlt_le_trans _ (CR_of_Q R q + CR_of_Q R (1#2))).
+    apply (CRplus_lt_compat_r (CR_of_Q R (1 # 2))) in c.
+    unfold CRminus in c. rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r in c. exact c.
+    rewrite (CR_of_Q_plus R 1 1), <- CRplus_assoc, <- (CR_of_Q_plus R _ 1).
+    apply CRplus_le_compat. apply CR_of_Q_le.
+    rewrite Qinv_plus_distr. apply Qlt_le_weak, Qlt_floor.
+    apply CR_of_Q_le. discriminate.
+Qed.
+
+Lemma CRplus_appart_reg_l : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R),
+    (r + r1) ≶ (r + r2) -> r1 ≶ r2.
+Proof.
+  intros. destruct H.
+  left. apply (CRplus_lt_reg_l R r), c.
+  right. apply (CRplus_lt_reg_l R r), c.
+Qed.
+
+Lemma CRplus_appart_reg_r : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R),
+    (r1 + r) ≶ (r2 + r) -> r1 ≶ r2.
+Proof.
+  intros. destruct H.
+  left. apply (CRplus_lt_reg_r r), c.
+  right. apply (CRplus_lt_reg_r r), c.
+Qed.
+
+Lemma CRmult_appart_reg_l
+  : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R),
+    0 < r -> (r * r1) ≶ (r * r2) -> r1 ≶ r2.
+Proof.
+  intros. destruct H0.
+  left. exact (CRmult_lt_reg_l r _ _ H c).
+  right. exact (CRmult_lt_reg_l r _ _ H c).
+Qed.
+
+Lemma CRmult_appart_reg_r
+  : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R),
+    0 < r -> (r1 * r) ≶ (r2 * r) -> r1 ≶ r2.
+Proof.
+  intros. destruct H0.
+  left. exact (CRmult_lt_reg_r r _ _ H c).
+  right. exact (CRmult_lt_reg_r r _ _ H c).
+Qed.
+
+Instance CRapart_morph
+  : forall {R : ConstructiveReals}, CMorphisms.Proper
+      (CMorphisms.respectful (CReq R) (CMorphisms.respectful (CReq R) CRelationClasses.iffT)) (CRapart R).
+Proof.
+  intros R x y H x0 y0 H0. destruct H, H0. split.
+  - intro. destruct H3.
+    left. apply (CRle_lt_trans _ x _ H).
+    apply (CRlt_le_trans _ x0 _ c), H2.
+    right. apply (CRle_lt_trans _ x0 _ H0).
+    apply (CRlt_le_trans _ x _ c), H1.
+  - intro. destruct H3.
+    left. apply (CRle_lt_trans _ y _ H1).
+    apply (CRlt_le_trans _ y0 _ c), H0.
+    right. apply (CRle_lt_trans _ y0 _ H2).
+    apply (CRlt_le_trans _ y _ c), H.
+Qed.
diff --git a/theories/Reals/Abstract/ConstructiveRealsMorphisms.v b/theories/Reals/Abstract/ConstructiveRealsMorphisms.v
new file mode 100644
index 0000000000..bc44668e2f
--- /dev/null
+++ b/theories/Reals/Abstract/ConstructiveRealsMorphisms.v
@@ -0,0 +1,1177 @@
+(************************************************************************)
+(*         *   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)         *)
+(************************************************************************)
+(************************************************************************)
+
+(** Morphisms used to transport results from any instance of
+    ConstructiveReals to any other.
+    Between any two constructive reals structures R1 and R2,
+    all morphisms R1 -> R2 are extensionally equal. We will
+    further show that they exist, and so are isomorphisms.
+    The difference between two morphisms R1 -> R2 is therefore
+    the speed of computation.
+
+    The canonical isomorphisms we provide here are often very slow,
+    when a new implementation of constructive reals is added,
+    it should define its own ad hoc isomorphisms for better speed.
+
+    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. *)
+
+Require Import QArith.
+Require Import Qabs.
+Require Import ConstructiveReals.
+Require Import ConstructiveLimits.
+Require Import ConstructiveAbs.
+Require Import ConstructiveSum.
+
+Local Open Scope ConstructiveReals.
+
+Record ConstructiveRealsMorphism {R1 R2 : ConstructiveReals} : Set :=
+  {
+    CRmorph : CRcarrier R1 -> CRcarrier R2;
+    CRmorph_rat : forall q : Q,
+        CRmorph (CR_of_Q R1 q) == CR_of_Q R2 q;
+    CRmorph_increasing : forall x y : CRcarrier R1,
+        CRlt R1 x y -> CRlt R2 (CRmorph x) (CRmorph y);
+  }.
+
+
+Lemma CRmorph_increasing_inv
+  : forall {R1 R2 : ConstructiveReals}
+      (f : ConstructiveRealsMorphism)
+      (x y : CRcarrier R1),
+    CRlt R2 (CRmorph f x) (CRmorph f y)
+    -> CRlt R1 x y.
+Proof.
+  intros. destruct (CR_Q_dense R2 _ _ H) as [q [H0 H1]].
+  destruct (CR_Q_dense R2 _ _ H0) as [r [H2 H3]].
+  apply lt_CR_of_Q, (CR_of_Q_lt R1) in H3.
+  destruct (CRltLinear R1).
+  destruct (s _ x _ H3).
+  - exfalso. apply (CRmorph_increasing f) in c.
+    destruct (CRmorph_rat f r) as [H4 _].
+    apply (CRle_lt_trans _ _ _ H4) in c. clear H4.
+    exact (CRlt_asym _ _ c H2).
+  - clear H2 H3 r. apply (CRlt_trans _ _ _ c). clear c.
+    destruct (CR_Q_dense R2 _ _ H1) as [t [H2 H3]].
+    apply lt_CR_of_Q, (CR_of_Q_lt R1) in H2.
+    destruct (s _ y _ H2). exact c.
+    exfalso. apply (CRmorph_increasing f) in c.
+    destruct (CRmorph_rat f t) as [_ H4].
+    apply (CRlt_le_trans _ _ _ c) in H4. clear c.
+    exact (CRlt_asym _ _ H4 H3).
+Qed.
+
+Lemma CRmorph_unique : forall {R1 R2 : ConstructiveReals}
+                         (f g : @ConstructiveRealsMorphism R1 R2)
+                         (x : CRcarrier R1),
+    CRmorph f x == CRmorph g x.
+Proof.
+  split.
+  - intro abs. destruct (CR_Q_dense R2 _ _ abs) as [q [H H0]].
+    destruct (CRmorph_rat f q) as [H1 _].
+    apply (CRlt_le_trans _ _ _ H) in H1. clear H.
+    apply CRmorph_increasing_inv in H1.
+    destruct (CRmorph_rat g q) as [_ H2].
+    apply (CRle_lt_trans _ _ _ H2) in H0. clear H2.
+    apply CRmorph_increasing_inv in H0.
+    exact (CRlt_asym _ _ H0 H1).
+  - intro abs. destruct (CR_Q_dense R2 _ _ abs) as [q [H H0]].
+    destruct (CRmorph_rat f q) as [_ H1].
+    apply (CRle_lt_trans _ _ _ H1) in H0. clear H1.
+    apply CRmorph_increasing_inv in H0.
+    destruct (CRmorph_rat g q) as [H2 _].
+    apply (CRlt_le_trans _ _ _ H) in H2. clear H.
+    apply CRmorph_increasing_inv in H2.
+    exact (CRlt_asym _ _ H0 H2).
+Qed.
+
+
+(* The identity is the only endomorphism of constructive reals.
+   For any ConstructiveReals R1, R2 and any morphisms
+   f : R1 -> R2 and g : R2 -> R1,
+   f and g are isomorphisms and are inverses of each other. *)
+Lemma Endomorph_id
+  : forall {R : ConstructiveReals} (f : @ConstructiveRealsMorphism R R)
+      (x : CRcarrier R),
+    CRmorph f x == x.
+Proof.
+  split.
+  - intro abs. destruct (CR_Q_dense R _ _ abs) as [q [H0 H1]].
+    destruct (CRmorph_rat f q) as [H _].
+    apply (CRlt_le_trans _ _ _ H0) in H. clear H0.
+    apply CRmorph_increasing_inv in H.
+    exact (CRlt_asym _ _ H1 H).
+  - intro abs. destruct (CR_Q_dense R _ _ abs) as [q [H0 H1]].
+    destruct (CRmorph_rat f q) as [_ H].
+    apply (CRle_lt_trans _ _ _ H) in H1. clear H.
+    apply CRmorph_increasing_inv in H1.
+    exact (CRlt_asym _ _ H1 H0).
+Qed.
+
+Lemma CRmorph_proper
+  : forall {R1 R2 : ConstructiveReals}
+      (f : @ConstructiveRealsMorphism R1 R2)
+      (x y : CRcarrier R1),
+    x == y -> CRmorph f x == CRmorph f y.
+Proof.
+  split.
+  - intro abs. apply CRmorph_increasing_inv in abs.
+    destruct H. contradiction.
+  - intro abs. apply CRmorph_increasing_inv in abs.
+    destruct H. contradiction.
+Qed.
+
+Definition CRmorph_compose {R1 R2 R3 : ConstructiveReals}
+           (f : @ConstructiveRealsMorphism R1 R2)
+           (g : @ConstructiveRealsMorphism R2 R3)
+  : @ConstructiveRealsMorphism R1 R3.
+Proof.
+  apply (Build_ConstructiveRealsMorphism
+           R1 R3 (fun x:CRcarrier R1 => CRmorph g (CRmorph f x))).
+  - intro q. apply (CReq_trans _ (CRmorph g (CR_of_Q R2 q))).
+    apply CRmorph_proper. apply CRmorph_rat. apply CRmorph_rat.
+  - intros. apply CRmorph_increasing. apply CRmorph_increasing. exact H.
+Defined.
+
+Lemma CRmorph_le : forall {R1 R2 : ConstructiveReals}
+                     (f : @ConstructiveRealsMorphism R1 R2)
+                     (x y : CRcarrier R1),
+    x <= y -> CRmorph f x <= CRmorph f y.
+Proof.
+  intros. intro abs. apply CRmorph_increasing_inv in abs. contradiction.
+Qed.
+
+Lemma CRmorph_le_inv : forall {R1 R2 : ConstructiveReals}
+                         (f : @ConstructiveRealsMorphism R1 R2)
+                         (x y : CRcarrier R1),
+    CRmorph f x <= CRmorph f y -> x <= y.
+Proof.
+  intros. intro abs. apply (CRmorph_increasing f) in abs. contradiction.
+Qed.
+
+Lemma CRmorph_zero : forall {R1 R2 : ConstructiveReals}
+                       (f : @ConstructiveRealsMorphism R1 R2),
+    CRmorph f 0 == 0.
+Proof.
+  intros. apply (CReq_trans _ (CRmorph f (CR_of_Q R1 0))).
+  apply CRmorph_proper. apply CReq_sym, CR_of_Q_zero.
+  apply (CReq_trans _ (CR_of_Q R2 0)).
+  apply CRmorph_rat. apply CR_of_Q_zero.
+Qed.
+
+Lemma CRmorph_one : forall {R1 R2 : ConstructiveReals}
+                      (f : @ConstructiveRealsMorphism R1 R2),
+    CRmorph f 1 == 1.
+Proof.
+  intros. apply (CReq_trans _ (CRmorph f (CR_of_Q R1 1))).
+  apply CRmorph_proper. apply CReq_sym, CR_of_Q_one.
+  apply (CReq_trans _ (CR_of_Q R2 1)).
+  apply CRmorph_rat. apply CR_of_Q_one.
+Qed.
+
+Lemma CRmorph_opp : forall {R1 R2 : ConstructiveReals}
+                      (f : @ConstructiveRealsMorphism R1 R2)
+                      (x : CRcarrier R1),
+    CRmorph f (- x) == - CRmorph f x.
+Proof.
+  split.
+  - intro abs.
+    destruct (CR_Q_dense R2 _ _ abs) as [q [H H0]]. clear abs.
+    destruct (CRmorph_rat f q) as [H1 _].
+    apply (CRlt_le_trans _ _ _ H) in H1. clear H.
+    apply CRmorph_increasing_inv in H1.
+    apply CRopp_gt_lt_contravar in H0.
+    destruct (@CR_of_Q_opp R2 q) as [H2 _].
+    apply (CRlt_le_trans _ _ _ H0) in H2. clear H0.
+    pose proof (CRopp_involutive (CRmorph f x)) as [H _].
+    apply (CRle_lt_trans _ _ _ H) in H2. clear H.
+    destruct (CRmorph_rat f (-q)) as [H _].
+    apply (CRlt_le_trans _ _ _ H2) in H. clear H2.
+    apply CRmorph_increasing_inv in H.
+    destruct (@CR_of_Q_opp R1 q) as [_ H2].
+    apply (CRlt_le_trans _ _ _ H) in H2. clear H.
+    apply CRopp_gt_lt_contravar in H2.
+    pose proof (CRopp_involutive (CR_of_Q R1 q)) as [H _].
+    apply (CRle_lt_trans _ _ _ H) in H2. clear H.
+    exact (CRlt_asym _ _ H1 H2).
+  - intro abs.
+    destruct (CR_Q_dense R2 _ _ abs) as [q [H H0]]. clear abs.
+    destruct (CRmorph_rat f q) as [_ H1].
+    apply (CRle_lt_trans _ _ _ H1) in H0. clear H1.
+    apply CRmorph_increasing_inv in H0.
+    apply CRopp_gt_lt_contravar in H.
+    pose proof (CRopp_involutive (CRmorph f x)) as [_ H1].
+    apply (CRlt_le_trans _ _ _ H) in H1. clear H.
+    destruct (@CR_of_Q_opp R2 q) as [_ H2].
+    apply (CRle_lt_trans _ _ _ H2) in H1. clear H2.
+    destruct (CRmorph_rat f (-q)) as [_ H].
+    apply (CRle_lt_trans _ _ _ H) in H1. clear H.
+    apply CRmorph_increasing_inv in H1.
+    destruct (@CR_of_Q_opp R1 q) as [H2 _].
+    apply (CRle_lt_trans _ _ _ H2) in H1. clear H2.
+    apply CRopp_gt_lt_contravar in H1.
+    pose proof (CRopp_involutive (CR_of_Q R1 q)) as [_ H].
+    apply (CRlt_le_trans _ _ _ H1) in H. clear H1.
+    exact (CRlt_asym _ _ H0 H).
+Qed.
+
+Lemma CRplus_pos_rat_lt : forall {R : ConstructiveReals} (x : CRcarrier R) (q : Q),
+    Qlt 0 q -> CRlt R x (CRplus R x (CR_of_Q R q)).
+Proof.
+  intros.
+  apply (CRle_lt_trans _ (CRplus R x (CRzero R))). apply CRplus_0_r.
+  apply CRplus_lt_compat_l.
+  apply (CRle_lt_trans _ (CR_of_Q R 0)). apply CR_of_Q_zero.
+  apply CR_of_Q_lt. exact H.
+Defined.
+
+Lemma CRplus_neg_rat_lt : forall {R : ConstructiveReals} (x : CRcarrier R) (q : Q),
+    Qlt q 0 -> CRlt R (CRplus R x (CR_of_Q R q)) x.
+Proof.
+  intros.
+  apply (CRlt_le_trans _ (CRplus R x (CRzero R))). 2: apply CRplus_0_r.
+  apply CRplus_lt_compat_l.
+  apply (CRlt_le_trans _ (CR_of_Q R 0)).
+  apply CR_of_Q_lt. exact H. apply CR_of_Q_zero.
+Qed.
+
+Lemma CRmorph_plus_rat : forall {R1 R2 : ConstructiveReals}
+                                (f : @ConstructiveRealsMorphism R1 R2)
+                                (x : CRcarrier R1) (q : Q),
+    CRmorph f (CRplus R1 x (CR_of_Q R1 q))
+    == CRplus R2 (CRmorph f x) (CR_of_Q R2 q).
+Proof.
+  split.
+  - intro abs.
+    destruct (CR_Q_dense R2 _ _ abs) as [r [H H0]]. clear abs.
+    destruct (CRmorph_rat f r) as [H1 _].
+    apply (CRlt_le_trans _ _ _ H) in H1. clear H.
+    apply CRmorph_increasing_inv in H1.
+    apply (CRlt_asym _ _ H1). clear H1.
+    apply (CRplus_lt_reg_r (CRopp R1 (CR_of_Q R1 q))).
+    apply (CRlt_le_trans _ x).
+    apply (CRle_lt_trans _ (CR_of_Q R1 (r-q))).
+    apply (CRle_trans _ (CRplus R1 (CR_of_Q R1 r) (CR_of_Q R1 (-q)))).
+    apply CRplus_le_compat_l. destruct (@CR_of_Q_opp R1 q). exact H.
+    destruct (CR_of_Q_plus R1 r (-q)). exact H.
+    apply (CRmorph_increasing_inv f).
+    apply (CRle_lt_trans _ (CR_of_Q R2 (r - q))).
+    apply CRmorph_rat.
+    apply (CRplus_lt_reg_r (CR_of_Q R2 q)).
+    apply (CRle_lt_trans _ (CR_of_Q R2 r)). 2: exact H0.
+    intro H.
+    destruct (CR_of_Q_plus R2 (r-q) q) as [H1 _].
+    apply (CRlt_le_trans _ _ _ H) in H1. clear H.
+    apply lt_CR_of_Q in H1. ring_simplify in H1.
+    exact (Qlt_not_le _ _ H1 (Qle_refl _)).
+    destruct (CRisRing R1).
+    apply (CRle_trans
+             _ (CRplus R1 x (CRplus R1 (CR_of_Q R1 q) (CRopp R1 (CR_of_Q R1 q))))).
+    apply (CRle_trans _ (CRplus R1 x (CRzero R1))).
+    destruct (CRplus_0_r x). exact H.
+    apply CRplus_le_compat_l. destruct (Ropp_def (CR_of_Q R1 q)). exact H.
+    destruct (Radd_assoc x (CR_of_Q R1 q) (CRopp R1 (CR_of_Q R1 q))).
+    exact H1.
+  - intro abs.
+    destruct (CR_Q_dense R2 _ _ abs) as [r [H H0]]. clear abs.
+    destruct (CRmorph_rat f r) as [_ H1].
+    apply (CRle_lt_trans _ _ _ H1) in H0. clear H1.
+    apply CRmorph_increasing_inv in H0.
+    apply (CRlt_asym _ _ H0). clear H0.
+    apply (CRplus_lt_reg_r (CRopp R1 (CR_of_Q R1 q))).
+    apply (CRle_lt_trans _ x).
+    destruct (CRisRing R1).
+    apply (CRle_trans
+             _ (CRplus R1 x (CRplus R1 (CR_of_Q R1 q) (CRopp R1 (CR_of_Q R1 q))))).
+    destruct (Radd_assoc x (CR_of_Q R1 q) (CRopp R1 (CR_of_Q R1 q))).
+    exact H0.
+    apply (CRle_trans _ (CRplus R1 x (CRzero R1))).
+    apply CRplus_le_compat_l. destruct (Ropp_def (CR_of_Q R1 q)). exact H1.
+    destruct (CRplus_0_r x). exact H1.
+    apply (CRlt_le_trans _ (CR_of_Q R1 (r-q))).
+    apply (CRmorph_increasing_inv f).
+    apply (CRlt_le_trans _ (CR_of_Q R2 (r - q))).
+    apply (CRplus_lt_reg_r (CR_of_Q R2 q)).
+    apply (CRlt_le_trans _ _ _ H).
+    2: apply CRmorph_rat.
+    apply (CRle_trans _ (CR_of_Q R2 (r-q+q))).
+    intro abs. apply lt_CR_of_Q in abs. ring_simplify in abs.
+    exact (Qlt_not_le _ _ abs (Qle_refl _)).
+    destruct (CR_of_Q_plus R2 (r-q) q). exact H1.
+    apply (CRle_trans _ (CRplus R1 (CR_of_Q R1 r) (CR_of_Q R1 (-q)))).
+    destruct (CR_of_Q_plus R1 r (-q)). exact H1.
+    apply CRplus_le_compat_l. destruct (@CR_of_Q_opp R1 q). exact H1.
+Qed.
+
+Lemma CRmorph_plus : forall {R1 R2 : ConstructiveReals}
+                       (f : @ConstructiveRealsMorphism R1 R2)
+                       (x y : CRcarrier R1),
+    CRmorph f (CRplus R1 x y)
+    == CRplus R2 (CRmorph f x) (CRmorph f y).
+Proof.
+  intros R1 R2 f.
+  assert (forall (x y : CRcarrier R1),
+             CRplus R2 (CRmorph f x) (CRmorph f y)
+             <= CRmorph f (CRplus R1 x y)).
+  { intros x y abs. destruct (CR_Q_dense R2 _ _ abs) as [r [H H0]]. clear abs.
+    destruct (CRmorph_rat f r) as [H1 _].
+    apply (CRlt_le_trans _ _ _ H) in H1. clear H.
+    apply CRmorph_increasing_inv in H1.
+    apply (CRlt_asym _ _ H1). clear H1.
+    destruct (CR_Q_dense R2 _ _ H0) as [q [H2 H3]].
+    apply lt_CR_of_Q in H2.
+    assert (Qlt (r-q) 0) as epsNeg.
+    { apply (Qplus_lt_r _ _ q). ring_simplify. exact H2. }
+    destruct (CR_Q_dense R1 _ _ (CRplus_neg_rat_lt x (r-q) epsNeg))
+      as [s [H4 H5]].
+    apply (CRlt_trans _ (CRplus R1 (CR_of_Q R1 s) y)).
+    2: apply CRplus_lt_compat_r, H5.
+    apply (CRmorph_increasing_inv f).
+    apply (CRlt_le_trans _ (CRplus R2 (CR_of_Q R2 s) (CRmorph f y))).
+    apply (CRmorph_increasing f) in H4.
+    destruct (CRmorph_plus_rat f x (r-q)) as [H _].
+    apply (CRle_lt_trans _ _ _ H) in H4. clear H.
+    destruct (CRmorph_rat f s) as [_ H1].
+    apply (CRlt_le_trans _ _ _ H4) in H1. clear H4.
+    apply (CRlt_trans
+             _ (CRplus R2 (CRplus R2 (CRmorph f x) (CR_of_Q R2 (r - q)))
+                       (CRmorph f y))).
+    2: apply CRplus_lt_compat_r, H1.
+    apply (CRlt_le_trans
+             _ (CRplus R2 (CRplus R2 (CR_of_Q R2 (r - q)) (CRmorph f x))
+                       (CRmorph f y))).
+    apply (CRlt_le_trans
+             _ (CRplus R2 (CR_of_Q R2 (r - q))
+                       (CRplus R2 (CRmorph f x) (CRmorph f y)))).
+    apply (CRle_lt_trans _ (CRplus R2 (CR_of_Q R2 (r - q)) (CR_of_Q R2 q))).
+    2: apply CRplus_lt_compat_l, H3.
+    intro abs.
+    destruct (CR_of_Q_plus R2 (r-q) q) as [_ H4].
+    apply (CRle_lt_trans _ _ _ H4) in abs. clear H4.
+    destruct (CRmorph_rat f r) as [_ H4].
+    apply (CRlt_le_trans _ _ _ abs) in H4. clear abs.
+    apply lt_CR_of_Q in H4. ring_simplify in H4.
+    exact (Qlt_not_le _ _ H4 (Qle_refl _)).
+    destruct (CRisRing R2); apply Radd_assoc.
+    apply CRplus_le_compat_r. destruct (CRisRing R2).
+    destruct (Radd_comm (CRmorph f x) (CR_of_Q R2 (r - q))).
+    exact H.
+    intro abs.
+    destruct (CRmorph_plus_rat f y s) as [H _]. apply H. clear H.
+    apply (CRlt_le_trans _ (CRplus R2 (CR_of_Q R2 s) (CRmorph f y))).
+    apply (CRle_lt_trans _ (CRmorph f (CRplus R1 (CR_of_Q R1 s) y))).
+    apply CRmorph_proper. destruct (CRisRing R1); apply Radd_comm.
+    exact abs. destruct (CRisRing R2); apply Radd_comm. }
+  split.
+  - apply H.
+  - specialize (H (CRplus R1 x y) (CRopp R1 y)).
+    intro abs. apply H. clear H.
+    apply (CRle_lt_trans _ (CRmorph f x)).
+    apply CRmorph_proper. destruct (CRisRing R1).
+    apply (CReq_trans _ (CRplus R1 x (CRplus R1 y (CRopp R1 y)))).
+    apply CReq_sym, Radd_assoc.
+    apply (CReq_trans _ (CRplus R1 x (CRzero R1))). 2: apply CRplus_0_r.
+    destruct (CRisRingExt R1). apply Radd_ext.
+    apply CReq_refl. apply Ropp_def.
+    apply (CRplus_lt_reg_r (CRmorph f y)).
+    apply (CRlt_le_trans _ _ _ abs). clear abs.
+    apply (CRle_trans _ (CRplus R2 (CRmorph f (CRplus R1 x y)) (CRzero R2))).
+    destruct (CRplus_0_r (CRmorph f (CRplus R1 x y))). exact H.
+    apply (CRle_trans _ (CRplus R2 (CRmorph f (CRplus R1 x y))
+                                (CRplus R2 (CRmorph f (CRopp R1 y)) (CRmorph f y)))).
+    apply CRplus_le_compat_l.
+    apply (CRle_trans
+             _ (CRplus R2 (CRopp R2 (CRmorph f y)) (CRmorph f y))).
+    destruct (CRplus_opp_l (CRmorph f y)). exact H.
+    apply CRplus_le_compat_r. destruct (CRmorph_opp f y). exact H.
+    destruct (CRisRing R2).
+    destruct (Radd_assoc (CRmorph f (CRplus R1 x y))
+                         (CRmorph f (CRopp R1 y)) (CRmorph f y)).
+    exact H0.
+Qed.
+
+Lemma CRmorph_mult_pos : forall {R1 R2 : ConstructiveReals}
+                           (f : @ConstructiveRealsMorphism R1 R2)
+                           (x : CRcarrier R1) (n : nat),
+    CRmorph f (CRmult R1 x (CR_of_Q R1 (Z.of_nat n # 1)))
+    == CRmult R2 (CRmorph f x) (CR_of_Q R2 (Z.of_nat n # 1)).
+Proof.
+  induction n.
+  - simpl. destruct (CRisRingExt R1).
+    apply (CReq_trans _ (CRzero R2)).
+    + apply (CReq_trans _ (CRmorph f (CRzero R1))).
+      2: apply CRmorph_zero. apply CRmorph_proper.
+      apply (CReq_trans _ (CRmult R1 x (CRzero R1))).
+      2: apply CRmult_0_r. apply Rmul_ext. apply CReq_refl. apply CR_of_Q_zero.
+    + apply (CReq_trans _ (CRmult R2 (CRmorph f x) (CRzero R2))).
+      apply CReq_sym, CRmult_0_r. destruct (CRisRingExt R2).
+      apply Rmul_ext0. apply CReq_refl. apply CReq_sym, CR_of_Q_zero.
+  - destruct (CRisRingExt R1), (CRisRingExt R2).
+    apply (CReq_trans
+             _  (CRmorph f (CRplus R1 x (CRmult R1 x (CR_of_Q R1 (Z.of_nat n # 1)))))).
+    apply CRmorph_proper.
+    apply (CReq_trans
+             _ (CRmult R1 x (CRplus R1 (CRone R1) (CR_of_Q R1 (Z.of_nat n # 1))))).
+    apply Rmul_ext. apply CReq_refl.
+    apply (CReq_trans _ (CR_of_Q R1 (1 + (Z.of_nat n # 1)))).
+    apply CR_of_Q_morph. rewrite Nat2Z.inj_succ. unfold Z.succ.
+    rewrite Z.add_comm. rewrite Qinv_plus_distr. reflexivity.
+    apply (CReq_trans _ (CRplus R1 (CR_of_Q R1 1) (CR_of_Q R1 (Z.of_nat n # 1)))).
+    apply CR_of_Q_plus. apply Radd_ext. apply CR_of_Q_one. apply CReq_refl.
+    apply (CReq_trans _ (CRplus R1 (CRmult R1 x (CRone R1))
+                                (CRmult R1 x (CR_of_Q R1 (Z.of_nat n # 1))))).
+    apply CRmult_plus_distr_l. apply Radd_ext. apply CRmult_1_r. apply CReq_refl.
+    apply (CReq_trans
+             _ (CRplus R2 (CRmorph f x)
+                       (CRmorph f (CRmult R1 x (CR_of_Q R1 (Z.of_nat n # 1)))))).
+    apply CRmorph_plus.
+    apply (CReq_trans
+             _ (CRplus R2 (CRmorph f x)
+                       (CRmult R2 (CRmorph f x) (CR_of_Q R2 (Z.of_nat n # 1))))).
+    apply Radd_ext0. apply CReq_refl. exact IHn.
+    apply (CReq_trans
+             _ (CRmult R2 (CRmorph f x) (CRplus R2 (CRone R2) (CR_of_Q R2 (Z.of_nat n # 1))))).
+    apply (CReq_trans
+             _ (CRplus R2 (CRmult R2 (CRmorph f x) (CRone R2))
+                       (CRmult R2 (CRmorph f x) (CR_of_Q R2 (Z.of_nat n # 1))))).
+    apply Radd_ext0. 2: apply CReq_refl. apply CReq_sym, CRmult_1_r.
+    apply CReq_sym, CRmult_plus_distr_l.
+    apply Rmul_ext0. apply CReq_refl.
+    apply (CReq_trans _ (CR_of_Q R2 (1 + (Z.of_nat n # 1)))).
+    apply (CReq_trans _ (CRplus R2 (CR_of_Q R2 1) (CR_of_Q R2 (Z.of_nat n # 1)))).
+    apply Radd_ext0. apply CReq_sym, CR_of_Q_one. apply CReq_refl.
+    apply CReq_sym, CR_of_Q_plus.
+    apply CR_of_Q_morph. rewrite Nat2Z.inj_succ. unfold Z.succ.
+    rewrite Z.add_comm. rewrite Qinv_plus_distr. reflexivity.
+Qed.
+
+Lemma NatOfZ : forall n : Z, { p : nat | n = Z.of_nat p \/ n = Z.opp (Z.of_nat p) }.
+Proof.
+  intros [|p|n].
+  - exists O. left. reflexivity.
+  - exists (Pos.to_nat p). left. rewrite positive_nat_Z. reflexivity.
+  - exists (Pos.to_nat n). right. rewrite positive_nat_Z. reflexivity.
+Qed.
+
+Lemma CRmorph_mult_int : forall {R1 R2 : ConstructiveReals}
+                           (f : @ConstructiveRealsMorphism R1 R2)
+                           (x : CRcarrier R1) (n : Z),
+    CRmorph f (CRmult R1 x (CR_of_Q R1 (n # 1)))
+    == CRmult R2 (CRmorph f x) (CR_of_Q R2 (n # 1)).
+Proof.
+  intros. destruct (NatOfZ n) as [p [pos|neg]].
+  - subst n. apply CRmorph_mult_pos.
+  - subst n.
+    apply (CReq_trans
+             _ (CRopp R2 (CRmorph  f (CRmult R1 x (CR_of_Q R1 (Z.of_nat p # 1)))))).
+    + apply (CReq_trans
+               _ (CRmorph f (CRopp R1 (CRmult R1 x (CR_of_Q R1 (Z.of_nat p # 1)))))).
+      2: apply CRmorph_opp. apply CRmorph_proper.
+      apply (CReq_trans _ (CRmult R1 x (CR_of_Q R1 (- (Z.of_nat p # 1))))).
+      destruct (CRisRingExt R1). apply Rmul_ext. apply CReq_refl.
+      apply CR_of_Q_morph. reflexivity.
+      apply (CReq_trans _ (CRmult R1 x (CRopp R1 (CR_of_Q R1 (Z.of_nat p # 1))))).
+      destruct (CRisRingExt R1). apply Rmul_ext. apply CReq_refl.
+      apply CR_of_Q_opp. apply CReq_sym, CRopp_mult_distr_r.
+    + apply (CReq_trans
+               _ (CRopp R2 (CRmult R2 (CRmorph f x) (CR_of_Q R2 (Z.of_nat p # 1))))).
+      destruct (CRisRingExt R2). apply Ropp_ext. apply CRmorph_mult_pos.
+      apply (CReq_trans
+               _ (CRmult R2 (CRmorph f x) (CRopp R2 (CR_of_Q R2 (Z.of_nat p # 1))))).
+      apply CRopp_mult_distr_r. destruct (CRisRingExt R2).
+      apply Rmul_ext. apply CReq_refl.
+      apply (CReq_trans _ (CR_of_Q R2 (- (Z.of_nat p # 1)))).
+      apply CReq_sym, CR_of_Q_opp. apply CR_of_Q_morph. reflexivity.
+Qed.
+
+Lemma CRmorph_mult_inv : forall {R1 R2 : ConstructiveReals}
+                           (f : @ConstructiveRealsMorphism R1 R2)
+                           (x : CRcarrier R1) (p : positive),
+    CRmorph f (CRmult R1 x (CR_of_Q R1 (1 # p)))
+    == CRmult R2 (CRmorph f x) (CR_of_Q R2 (1 # p)).
+Proof.
+  intros. apply (CRmult_eq_reg_r (CR_of_Q R2 (Z.pos p # 1))).
+  left. apply (CRle_lt_trans _ (CR_of_Q R2 0)).
+  apply CR_of_Q_zero. apply CR_of_Q_lt. reflexivity.
+  apply (CReq_trans _ (CRmorph f x)).
+  - apply (CReq_trans
+             _ (CRmorph f (CRmult R1 (CRmult R1 x (CR_of_Q R1 (1 # p)))
+                                  (CR_of_Q R1 (Z.pos p # 1))))).
+    apply CReq_sym, CRmorph_mult_int. apply CRmorph_proper.
+    apply (CReq_trans
+             _ (CRmult R1 x (CRmult R1 (CR_of_Q R1 (1 # p))
+                                    (CR_of_Q R1 (Z.pos p # 1))))).
+    destruct (CRisRing R1). apply CReq_sym, Rmul_assoc.
+    apply (CReq_trans _ (CRmult R1 x (CRone R1))).
+    apply (Rmul_ext (CRisRingExt R1)). apply CReq_refl.
+    apply (CReq_trans _ (CR_of_Q R1 ((1#p) * (Z.pos p # 1)))).
+    apply CReq_sym, CR_of_Q_mult.
+    apply (CReq_trans _ (CR_of_Q R1 1)).
+    apply CR_of_Q_morph. reflexivity. apply CR_of_Q_one.
+    apply CRmult_1_r.
+  - apply (CReq_trans
+             _ (CRmult R2 (CRmorph f x)
+                       (CRmult R2 (CR_of_Q R2 (1 # p)) (CR_of_Q R2 (Z.pos p # 1))))).
+    2: apply (Rmul_assoc (CRisRing R2)).
+    apply (CReq_trans _ (CRmult R2 (CRmorph f x) (CRone R2))).
+    apply CReq_sym, CRmult_1_r.
+    apply (Rmul_ext (CRisRingExt R2)). apply CReq_refl.
+    apply (CReq_trans _ (CR_of_Q R2 1)).
+    apply CReq_sym, CR_of_Q_one.
+    apply (CReq_trans _ (CR_of_Q R2 ((1#p)*(Z.pos p # 1)))).
+    apply CR_of_Q_morph. reflexivity. apply CR_of_Q_mult.
+Qed.
+
+Lemma CRmorph_mult_rat : forall {R1 R2 : ConstructiveReals}
+                           (f : @ConstructiveRealsMorphism R1 R2)
+                           (x : CRcarrier R1) (q : Q),
+    CRmorph f (CRmult R1 x (CR_of_Q R1 q))
+    == CRmult R2 (CRmorph f x) (CR_of_Q R2 q).
+Proof.
+  intros. destruct q as [a b].
+  apply (CReq_trans
+           _ (CRmult R2 (CRmorph f (CRmult R1 x (CR_of_Q R1 (a # 1))))
+                     (CR_of_Q R2 (1 # b)))).
+  - apply (CReq_trans
+             _ (CRmorph f (CRmult R1 (CRmult R1 x (CR_of_Q R1 (a # 1)))
+                                  (CR_of_Q R1 (1 # b))))).
+    2: apply CRmorph_mult_inv. apply CRmorph_proper.
+    apply (CReq_trans
+             _ (CRmult R1 x (CRmult R1 (CR_of_Q R1 (a # 1))
+                                    (CR_of_Q R1 (1 # b))))).
+    apply (Rmul_ext (CRisRingExt R1)). apply CReq_refl.
+    apply (CReq_trans _ (CR_of_Q R1 ((a#1)*(1#b)))).
+    apply CR_of_Q_morph. unfold Qeq; simpl. rewrite Z.mul_1_r. reflexivity.
+    apply CR_of_Q_mult.
+    apply (Rmul_assoc (CRisRing R1)).
+  - apply (CReq_trans
+             _ (CRmult R2 (CRmult R2 (CRmorph f x) (CR_of_Q R2 (a # 1)))
+                       (CR_of_Q R2 (1 # b)))).
+    apply (Rmul_ext (CRisRingExt R2)). apply CRmorph_mult_int.
+    apply CReq_refl.
+    apply (CReq_trans
+             _ (CRmult R2 (CRmorph f x)
+                       (CRmult R2 (CR_of_Q R2 (a # 1)) (CR_of_Q R2 (1 # b))))).
+    apply CReq_sym, (Rmul_assoc (CRisRing R2)).
+    apply (Rmul_ext (CRisRingExt R2)). apply CReq_refl.
+    apply (CReq_trans _ (CR_of_Q R2 ((a#1)*(1#b)))).
+    apply CReq_sym, CR_of_Q_mult.
+    apply CR_of_Q_morph. unfold Qeq; simpl. rewrite Z.mul_1_r. reflexivity.
+Qed.
+
+Lemma CRmorph_mult_pos_pos_le : forall {R1 R2 : ConstructiveReals}
+                                  (f : @ConstructiveRealsMorphism R1 R2)
+                                  (x y : CRcarrier R1),
+    CRlt R1 (CRzero R1) y
+    -> CRmult R2 (CRmorph f x) (CRmorph f y)
+       <= CRmorph f (CRmult R1 x y).
+Proof.
+  intros. intro abs. destruct (CR_Q_dense R2 _ _ abs) as [q [H1 H2]].
+  destruct (CRmorph_rat f q) as [H3 _].
+  apply (CRlt_le_trans _ _ _ H1) in H3. clear H1.
+  apply CRmorph_increasing_inv in H3.
+  apply (CRlt_asym _ _ H3). clear H3.
+  destruct (CR_Q_dense R2 _ _ H2) as [r [H1 H3]].
+  apply lt_CR_of_Q in H1.
+  destruct (CR_archimedean R1 y) as [A Amaj].
+  assert (/ ((r - q) * (1 # A)) * (q - r) == - (Z.pos A # 1))%Q as diveq.
+  { rewrite Qinv_mult_distr. setoid_replace (q-r)%Q with (-1*(r-q))%Q.
+    field_simplify. reflexivity. 2: field.
+    split. intro H4. inversion H4. intro H4.
+    apply Qlt_minus_iff in H1. rewrite H4 in H1. inversion H1. }
+  destruct (CR_Q_dense R1 (CRplus R1 x (CR_of_Q R1 ((q-r) * (1#A)))) x)
+    as [s [H4 H5]].
+  - apply (CRlt_le_trans _ (CRplus R1 x (CRzero R1))).
+    2: apply CRplus_0_r. apply CRplus_lt_compat_l.
+    apply (CRplus_lt_reg_l R1 (CR_of_Q R1 ((r-q) * (1#A)))).
+    apply (CRle_lt_trans _ (CRzero R1)).
+    apply (CRle_trans _ (CR_of_Q R1 ((r-q)*(1#A) + (q-r)*(1#A)))).
+    destruct (CR_of_Q_plus R1 ((r-q)*(1#A)) ((q-r)*(1#A))).
+    exact H0. apply (CRle_trans _ (CR_of_Q R1 0)).
+    2: destruct (@CR_of_Q_zero R1); exact H4.
+    intro H4. apply lt_CR_of_Q in H4. ring_simplify in H4.
+    inversion H4.
+    apply (CRlt_le_trans _ (CR_of_Q R1 ((r - q) * (1 # A)))).
+    2: apply CRplus_0_r.
+    apply (CRle_lt_trans _ (CR_of_Q R1 0)).
+    apply CR_of_Q_zero. apply CR_of_Q_lt.
+    rewrite <- (Qmult_0_r (r-q)). apply Qmult_lt_l.
+    apply Qlt_minus_iff in H1. exact H1. reflexivity.
+  - apply (CRmorph_increasing f) in H4.
+    destruct (CRmorph_plus f x (CR_of_Q R1 ((q-r) * (1#A)))) as [H6 _].
+    apply (CRle_lt_trans _ _ _ H6) in H4. clear H6.
+    destruct (CRmorph_rat f s) as [_ H6].
+    apply (CRlt_le_trans _ _ _ H4) in H6. clear H4.
+    apply (CRmult_lt_compat_r (CRmorph f y)) in H6.
+    destruct (Rdistr_l (CRisRing R2) (CRmorph f x)
+                       (CRmorph f (CR_of_Q R1 ((q-r) * (1#A))))
+                       (CRmorph f y)) as [H4 _].
+    apply (CRle_lt_trans _ _ _ H4) in H6. clear H4.
+    apply (CRle_lt_trans _ (CRmult R1 (CR_of_Q R1 s) y)).
+    2: apply CRmult_lt_compat_r. 2: exact H. 2: exact H5.
+    apply (CRmorph_le_inv f).
+    apply (CRle_trans _ (CR_of_Q R2 q)).
+    destruct (CRmorph_rat f q). exact H4.
+    apply (CRle_trans _ (CRmult R2 (CR_of_Q R2 s) (CRmorph f y))).
+    apply (CRle_trans _ (CRplus R2 (CRmult R2 (CRmorph f x) (CRmorph f y))
+                                   (CR_of_Q R2 (q-r)))).
+    apply (CRle_trans _ (CRplus R2 (CR_of_Q R2 r) (CR_of_Q R2 (q - r)))).
+    + apply (CRle_trans _ (CR_of_Q R2 (r + (q-r)))).
+      intro H4. apply lt_CR_of_Q in H4. ring_simplify in H4.
+      exact (Qlt_not_le q q H4 (Qle_refl q)).
+      destruct (CR_of_Q_plus R2 r (q-r)). exact H4.
+    + apply CRplus_le_compat_r. intro H4.
+      apply (CRlt_asym _ _ H3). exact H4.
+    + intro H4. apply (CRlt_asym _ _ H4). clear H4.
+      apply (CRlt_trans_flip _ _ _ H6). clear H6.
+      apply CRplus_lt_compat_l.
+      apply (CRlt_le_trans
+               _ (CRmult R2 (CR_of_Q R2 ((q - r) * (1 # A))) (CRmorph f y))).
+      apply (CRmult_lt_reg_l (CR_of_Q R2 (/((r-q)*(1#A))))).
+      apply (CRle_lt_trans _ (CR_of_Q R2 0)). apply CR_of_Q_zero.
+      apply CR_of_Q_lt, Qinv_lt_0_compat.
+      rewrite <- (Qmult_0_r (r-q)). apply Qmult_lt_l.
+      apply Qlt_minus_iff in H1. exact H1. reflexivity.
+      apply (CRle_lt_trans _ (CRopp R2 (CR_of_Q R2 (Z.pos A # 1)))).
+      apply (CRle_trans _ (CR_of_Q R2 (-(Z.pos A # 1)))).
+      apply (CRle_trans _ (CR_of_Q R2 ((/ ((r - q) * (1 # A))) * (q - r)))).
+      destruct (CR_of_Q_mult R2 (/ ((r - q) * (1 # A))) (q - r)).
+      exact H0. destruct (CR_of_Q_morph R2 (/ ((r - q) * (1 # A)) * (q - r))
+                                         (-(Z.pos A # 1))).
+      exact diveq. intro H7. apply lt_CR_of_Q in H7.
+      rewrite diveq in H7. exact (Qlt_not_le _ _ H7 (Qle_refl _)).
+      destruct (@CR_of_Q_opp R2 (Z.pos A # 1)). exact H4.
+      apply (CRlt_le_trans _ (CRopp R2 (CRmorph f y))).
+      apply CRopp_gt_lt_contravar.
+      apply (CRlt_le_trans _ (CRmorph f (CR_of_Q R1 (Z.pos A # 1)))).
+      apply CRmorph_increasing. exact Amaj.
+      destruct (CRmorph_rat f (Z.pos A # 1)). exact H4.
+      apply (CRle_trans _ (CRmult R2 (CRopp R2 (CRone R2)) (CRmorph f y))).
+      apply (CRle_trans _ (CRopp R2 (CRmult R2 (CRone R2) (CRmorph f y)))).
+      destruct (Ropp_ext (CRisRingExt R2) (CRmorph f y)
+                         (CRmult R2 (CRone R2) (CRmorph f y))).
+      apply CReq_sym, (Rmul_1_l (CRisRing R2)). exact H4.
+      destruct (CRopp_mult_distr_l (CRone R2) (CRmorph f y)). exact H4.
+      apply (CRle_trans _ (CRmult R2 (CRmult R2 (CR_of_Q R2 (/ ((r - q) * (1 # A))))
+                                             (CR_of_Q R2 ((q - r) * (1 # A))))
+                                  (CRmorph f y))).
+      apply CRmult_le_compat_r_half.
+      apply (CRle_lt_trans _ (CRmorph f (CRzero R1))).
+      apply CRmorph_zero. apply CRmorph_increasing. exact H.
+      apply (CRle_trans _ (CR_of_Q R2 ((/ ((r - q) * (1 # A)))
+                                       * ((q - r) * (1 # A))))).
+      apply (CRle_trans _ (CR_of_Q R2 (-1))).
+      apply (CRle_trans _ (CRopp R2 (CR_of_Q R2 1))).
+      destruct (Ropp_ext (CRisRingExt R2) (CRone R2) (CR_of_Q R2 1)).
+      apply CReq_sym, CR_of_Q_one. exact H4.
+      destruct (@CR_of_Q_opp R2 1). exact H0.
+      destruct (CR_of_Q_morph R2 (-1) (/ ((r - q) * (1 # A)) * ((q - r) * (1 # A)))).
+      field. split.
+      intro H4. inversion H4. intro H4. apply Qlt_minus_iff in H1.
+      rewrite H4 in H1. inversion H1. exact H4.
+      destruct (CR_of_Q_mult R2 (/ ((r - q) * (1 # A))) ((q - r) * (1 # A))).
+      exact H4.
+      destruct (Rmul_assoc (CRisRing R2) (CR_of_Q R2 (/ ((r - q) * (1 # A))))
+                           (CR_of_Q R2 ((q - r) * (1 # A)))
+                           (CRmorph f y)).
+      exact H0.
+      apply CRmult_le_compat_r_half.
+      apply (CRle_lt_trans _ (CRmorph f (CRzero R1))).
+      apply CRmorph_zero. apply CRmorph_increasing. exact H.
+      destruct (CRmorph_rat f ((q - r) * (1 # A))). exact H0.
+    + apply (CRle_trans _ (CRmorph f (CRmult R1 y (CR_of_Q R1 s)))).
+      apply (CRle_trans _ (CRmult R2 (CRmorph f y) (CR_of_Q R2 s))).
+      destruct (Rmul_comm (CRisRing R2) (CRmorph f y) (CR_of_Q R2 s)).
+      exact H0.
+      destruct (CRmorph_mult_rat f y s). exact H0.
+      destruct (CRmorph_proper f (CRmult R1 y (CR_of_Q R1 s))
+                               (CRmult R1 (CR_of_Q R1 s) y)).
+      apply (Rmul_comm (CRisRing R1)). exact H4.
+    + apply (CRle_lt_trans _ (CRmorph f (CRzero R1))).
+      apply CRmorph_zero. apply CRmorph_increasing. exact H.
+Qed.
+
+Lemma CRmorph_mult_pos_pos : forall {R1 R2 : ConstructiveReals}
+                               (f : @ConstructiveRealsMorphism R1 R2)
+                               (x y : CRcarrier R1),
+    CRlt R1 (CRzero R1) y
+    -> CRmorph f (CRmult R1 x y)
+       == CRmult R2 (CRmorph f x) (CRmorph f y).
+Proof.
+  split. apply CRmorph_mult_pos_pos_le. exact H.
+  intro abs. destruct (CR_Q_dense R2 _ _ abs) as [q [H1 H2]].
+  destruct (CRmorph_rat f q) as [_ H3].
+  apply (CRle_lt_trans _ _ _ H3) in H2. clear H3.
+  apply CRmorph_increasing_inv in H2.
+  apply (CRlt_asym _ _ H2). clear H2.
+  destruct (CR_Q_dense R2 _ _ H1) as [r [H2 H3]].
+  apply lt_CR_of_Q in H3.
+  destruct (CR_archimedean R1 y) as [A Amaj].
+  destruct (CR_Q_dense R1 x (CRplus R1 x (CR_of_Q R1 ((q-r) * (1#A)))))
+    as [s [H4 H5]].
+  - apply (CRle_lt_trans _ (CRplus R1 x (CRzero R1))).
+    apply CRplus_0_r. apply CRplus_lt_compat_l.
+    apply (CRle_lt_trans _ (CR_of_Q R1 0)).
+    apply CR_of_Q_zero. apply CR_of_Q_lt.
+    rewrite <- (Qmult_0_r (q-r)). apply Qmult_lt_l.
+    apply Qlt_minus_iff in H3. exact H3. reflexivity.
+  - apply (CRmorph_increasing f) in H5.
+    destruct (CRmorph_plus f x (CR_of_Q R1 ((q-r) * (1#A)))) as [_ H6].
+    apply (CRlt_le_trans _ _ _ H5) in H6. clear H5.
+    destruct (CRmorph_rat f s) as [H5 _ ].
+    apply (CRle_lt_trans _ _ _ H5) in H6. clear H5.
+    apply (CRmult_lt_compat_r (CRmorph f y)) in H6.
+    apply (CRlt_le_trans _ (CRmult R1 (CR_of_Q R1 s) y)).
+    apply CRmult_lt_compat_r. exact H. exact H4. clear H4.
+    apply (CRmorph_le_inv f).
+    apply (CRle_trans _ (CR_of_Q R2 q)).
+    2: destruct (CRmorph_rat f q); exact H0.
+    apply (CRle_trans _ (CRmult R2 (CR_of_Q R2 s) (CRmorph f y))).
+    + apply (CRle_trans _ (CRmorph f (CRmult R1 y (CR_of_Q R1 s)))).
+      destruct (CRmorph_proper f (CRmult R1 (CR_of_Q R1 s) y)
+                               (CRmult R1 y (CR_of_Q R1 s))).
+      apply (Rmul_comm (CRisRing R1)). exact H4.
+      apply (CRle_trans _ (CRmult R2 (CRmorph f y) (CR_of_Q R2 s))).
+      exact (proj2 (CRmorph_mult_rat f y s)).
+      destruct (Rmul_comm (CRisRing R2) (CR_of_Q R2 s) (CRmorph f y)).
+      exact H0.
+    + intro H5. apply (CRlt_asym _ _ H5). clear H5.
+      apply (CRlt_trans _ _ _ H6). clear H6.
+      apply (CRle_lt_trans
+               _ (CRplus R2
+                         (CRmult R2 (CRmorph f x) (CRmorph f y))
+                         (CRmult R2 (CRmorph f (CR_of_Q R1 ((q - r) * (1 # A))))
+                                 (CRmorph f y)))).
+      apply (Rdistr_l (CRisRing R2)).
+      apply (CRle_lt_trans
+               _ (CRplus R2 (CR_of_Q R2 r)
+                         (CRmult R2 (CRmorph f (CR_of_Q R1 ((q - r) * (1 # A))))
+                                 (CRmorph f y)))).
+      apply CRplus_le_compat_r. intro H5. apply (CRlt_asym _ _ H5 H2).
+      clear H2.
+      apply (CRle_lt_trans
+               _ (CRplus R2 (CR_of_Q R2 r)
+                         (CRmult R2 (CR_of_Q R2 ((q - r) * (1 # A)))
+                                 (CRmorph f y)))).
+      apply CRplus_le_compat_l, CRmult_le_compat_r_half.
+      apply (CRle_lt_trans _ (CRmorph f (CRzero R1))).
+      apply CRmorph_zero. apply CRmorph_increasing. exact H.
+      destruct (CRmorph_rat f ((q - r) * (1 # A))). exact H2.
+      apply (CRlt_le_trans _ (CRplus R2 (CR_of_Q R2 r)
+                                     (CR_of_Q R2 ((q - r))))).
+      apply CRplus_lt_compat_l.
+      * apply (CRmult_lt_reg_l (CR_of_Q R2 (/((q - r) * (1 # A))))).
+        apply (CRle_lt_trans _ (CR_of_Q R2 0)). apply CR_of_Q_zero.
+        apply CR_of_Q_lt, Qinv_lt_0_compat.
+        rewrite <- (Qmult_0_r (q-r)). apply Qmult_lt_l.
+        apply Qlt_minus_iff in H3. exact H3. reflexivity.
+        apply (CRle_lt_trans _ (CRmorph f y)).
+        apply (CRle_trans _ (CRmult R2 (CRmult R2 (CR_of_Q R2 (/ ((q - r) * (1 # A))))
+                                               (CR_of_Q R2 ((q - r) * (1 # A))))
+                                    (CRmorph f y))).
+        exact (proj2 (Rmul_assoc (CRisRing R2) (CR_of_Q R2 (/ ((q - r) * (1 # A))))
+                                 (CR_of_Q R2 ((q - r) * (1 # A)))
+                                 (CRmorph f y))).
+        apply (CRle_trans _ (CRmult R2 (CRone R2) (CRmorph f y))).
+        apply CRmult_le_compat_r_half.
+        apply (CRle_lt_trans _ (CRmorph f (CRzero R1))).
+        apply CRmorph_zero. apply CRmorph_increasing. exact H.
+        apply (CRle_trans
+                 _ (CR_of_Q R2 ((/ ((q - r) * (1 # A))) * ((q - r) * (1 # A))))).
+        exact (proj1 (CR_of_Q_mult R2 (/ ((q - r) * (1 # A))) ((q - r) * (1 # A)))).
+        apply (CRle_trans _ (CR_of_Q R2 1)).
+        destruct (CR_of_Q_morph R2 (/ ((q - r) * (1 # A)) * ((q - r) * (1 # A))) 1).
+        field_simplify. reflexivity. split.
+        intro H5. inversion H5. intro H5. apply Qlt_minus_iff in H3.
+        rewrite H5 in H3. inversion H3. exact H2.
+        destruct (CR_of_Q_one R2). exact H2.
+        destruct (Rmul_1_l (CRisRing R2) (CRmorph f y)).
+        intro H5. contradiction.
+        apply (CRlt_le_trans _ (CR_of_Q R2 (Z.pos A # 1))).
+        apply (CRlt_le_trans _ (CRmorph f (CR_of_Q R1 (Z.pos A # 1)))).
+        apply CRmorph_increasing. exact Amaj.
+        exact (proj2 (CRmorph_rat f (Z.pos A # 1))).
+        apply (CRle_trans _ (CR_of_Q R2 ((/ ((q - r) * (1 # A))) * (q - r)))).
+        2: exact (proj2 (CR_of_Q_mult R2 (/ ((q - r) * (1 # A))) (q - r))).
+        destruct (CR_of_Q_morph R2 (Z.pos A # 1) (/ ((q - r) * (1 # A)) * (q - r))).
+        field_simplify. reflexivity. split.
+        intro H5. inversion H5. intro H5. apply Qlt_minus_iff in H3.
+        rewrite H5 in H3. inversion H3. exact H2.
+      * apply (CRle_trans _ (CR_of_Q R2 (r + (q-r)))).
+        exact (proj1 (CR_of_Q_plus R2 r (q-r))).
+        destruct (CR_of_Q_morph R2 (r + (q-r)) q). ring. exact H2.
+    + apply (CRle_lt_trans _ (CRmorph f (CRzero R1))).
+      apply CRmorph_zero. apply CRmorph_increasing. exact H.
+Qed.
+
+Lemma CRmorph_mult : forall {R1 R2 : ConstructiveReals}
+                       (f : @ConstructiveRealsMorphism R1 R2)
+                       (x y : CRcarrier R1),
+    CRmorph f (CRmult R1 x y)
+    == CRmult R2 (CRmorph f x) (CRmorph f y).
+Proof.
+  intros.
+  destruct (CR_archimedean R1 (CRopp R1 y)) as [p pmaj].
+  apply (CRplus_eq_reg_r (CRmult R2 (CRmorph f x)
+                                    (CR_of_Q R2 (Z.pos p # 1)))).
+  apply (CReq_trans _ (CRmorph f (CRmult R1 x (CRplus R1 y (CR_of_Q R1 (Z.pos p # 1)))))).
+  - apply (CReq_trans _ (CRplus R2 (CRmorph f (CRmult R1 x y))
+                                (CRmorph f (CRmult R1 x (CR_of_Q R1 (Z.pos p # 1)))))).
+    apply (Radd_ext (CRisRingExt R2)). apply CReq_refl.
+    apply CReq_sym, CRmorph_mult_int.
+    apply (CReq_trans _ (CRmorph f (CRplus R1 (CRmult R1 x y)
+                                           (CRmult R1 x (CR_of_Q R1 (Z.pos p # 1)))))).
+    apply CReq_sym, CRmorph_plus. apply CRmorph_proper.
+    apply CReq_sym, CRmult_plus_distr_l.
+  - apply (CReq_trans _ (CRmult R2 (CRmorph f x)
+                                (CRmorph f (CRplus R1 y (CR_of_Q R1 (Z.pos p # 1)))))).
+    apply CRmorph_mult_pos_pos.
+    apply (CRplus_lt_compat_l R1 y) in pmaj.
+    apply (CRle_lt_trans _ (CRplus R1 y (CRopp R1 y))).
+    2: exact pmaj. apply (CRisRing R1).
+    apply (CReq_trans _ (CRmult R2 (CRmorph f x)
+                                (CRplus R2 (CRmorph f y) (CR_of_Q R2 (Z.pos p # 1))))).
+    apply (Rmul_ext (CRisRingExt R2)). apply CReq_refl.
+    apply (CReq_trans _ (CRplus R2 (CRmorph f y)
+                                (CRmorph f (CR_of_Q R1 (Z.pos p # 1))))).
+    apply CRmorph_plus.
+    apply (Radd_ext (CRisRingExt R2)). apply CReq_refl.
+    apply CRmorph_rat.
+    apply CRmult_plus_distr_l.
+Qed.
+
+Lemma CRmorph_appart : forall {R1 R2 : ConstructiveReals}
+                         (f : @ConstructiveRealsMorphism R1 R2)
+                         (x y : CRcarrier R1)
+                         (app : x ≶ y),
+    CRmorph f x ≶ CRmorph f y.
+Proof.
+  intros. destruct app.
+  - left. apply CRmorph_increasing. exact c.
+  - right. apply CRmorph_increasing. exact c.
+Defined.
+
+Lemma CRmorph_appart_zero : forall {R1 R2 : ConstructiveReals}
+                              (f : @ConstructiveRealsMorphism R1 R2)
+                              (x : CRcarrier R1)
+                              (app : x ≶ 0),
+    CRmorph f x ≶ 0.
+Proof.
+  intros. destruct app.
+  - left. apply (CRlt_le_trans _ (CRmorph f (CRzero R1))).
+    apply CRmorph_increasing. exact c.
+    exact (proj2 (CRmorph_zero f)).
+  - right. apply (CRle_lt_trans  _ (CRmorph f (CRzero R1))).
+    exact (proj1 (CRmorph_zero f)).
+    apply CRmorph_increasing. exact c.
+Defined.
+
+Lemma CRmorph_inv : forall {R1 R2 : ConstructiveReals}
+                      (f : @ConstructiveRealsMorphism R1 R2)
+                      (x : CRcarrier R1)
+                      (xnz : x ≶ 0)
+                      (fxnz : CRmorph f x ≶ 0),
+    CRmorph f ((/ x) xnz)
+    == (/ CRmorph f x) fxnz.
+Proof.
+  intros. apply (CRmult_eq_reg_r (CRmorph f x)).
+  destruct fxnz. right. exact c. left. exact c.
+  apply (CReq_trans _ (CRone R2)).
+  2: apply CReq_sym, CRinv_l.
+  apply (CReq_trans _ (CRmorph f (CRmult R1 ((/ x) xnz) x))).
+  apply CReq_sym, CRmorph_mult.
+  apply (CReq_trans _ (CRmorph f 1)).
+  apply CRmorph_proper. apply CRinv_l.
+  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_one, <- CR_of_Q_plus.
+    apply CR_of_Q_morph. rewrite Qinv_plus_distr.
+    unfold Qeq, Qnum, Qden. do 2 rewrite Z.mul_1_r.
+    rewrite Nat2Z.inj_succ. rewrite <- Z.add_1_l. reflexivity.
+    rewrite <- CR_of_Q_one, <- CR_of_Q_plus.
+    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),
+  CR_cauchy R1 (fun n => CR_of_Q R1 (qn n))
+  -> CR_cauchy R2 (fun n => CR_of_Q R2 (qn n)).
+Proof.
+  intros. intro p. destruct (H p) as [n nmaj].
+  exists n. intros. specialize (nmaj i j H0 H1).
+  unfold CRminus. rewrite <- CR_of_Q_opp, <- CR_of_Q_plus, CR_of_Q_abs.
+  unfold CRminus in nmaj. rewrite <- CR_of_Q_opp, <- CR_of_Q_plus, CR_of_Q_abs in nmaj.
+  apply CR_of_Q_le. destruct (Q_dec (Qabs (qn i + - qn j)) (1#p)).
+  destruct s. apply Qlt_le_weak, q. exfalso.
+  apply (Qlt_not_le _ _ q). apply (CR_of_Q_lt R1) in q. contradiction.
+  rewrite q. apply Qle_refl.
+Qed.
+
+Definition CR_Q_limit {R : ConstructiveReals} (x : CRcarrier R) (n:nat)
+  : { q:Q  &  x < CR_of_Q R q < x + CR_of_Q R (1 # Pos.of_nat n) }.
+Proof.
+  apply (CR_Q_dense R x (x + CR_of_Q R (1 # Pos.of_nat n))).
+  rewrite <- (CRplus_0_r x). rewrite CRplus_assoc.
+  apply CRplus_lt_compat_l. rewrite CRplus_0_l. apply CR_of_Q_pos.
+  reflexivity.
+Qed.
+
+Lemma CR_Q_limit_cv : forall {R : ConstructiveReals} (x : CRcarrier R),
+    CR_cv R (fun n => CR_of_Q R (let (q,_) := CR_Q_limit x n in q)) x.
+Proof.
+  intros R x p. exists (Pos.to_nat p).
+  intros. destruct (CR_Q_limit x i). rewrite CRabs_right.
+  apply (CRplus_le_reg_r x). unfold CRminus.
+  rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r, CRplus_comm.
+  apply (CRle_trans _ (x + CR_of_Q R (1 # Pos.of_nat i))).
+  apply CRlt_asym, p0. apply CRplus_le_compat_l, CR_of_Q_le.
+  unfold Qle, Qnum, Qden. rewrite Z.mul_1_l, Z.mul_1_l.
+  apply Pos2Z.pos_le_pos, Pos2Nat.inj_le. rewrite Nat2Pos.id. exact H.
+  destruct i. exfalso. inversion H. pose proof (Pos2Nat.is_pos p).
+  rewrite H1 in H0. inversion H0. discriminate.
+  rewrite <- (CRplus_opp_r x). apply CRplus_le_compat_r, CRlt_asym, p0.
+Qed.
+
+(* We call this morphism slow to remind that it should only be used
+   for proofs, not for computations. *)
+Definition SlowMorph {R1 R2 : ConstructiveReals}
+  : CRcarrier R1 -> CRcarrier R2
+  := fun x => let (y,_) := CR_complete R2 _ (CRmorph_rat_cv _ (Rcv_cauchy_mod _ x (CR_Q_limit_cv x)))
+              in y.
+
+Lemma CauchyMorph_rat : forall {R1 R2 : ConstructiveReals} (q : Q),
+    SlowMorph (CR_of_Q R1 q) == CR_of_Q R2 q.
+Proof.
+  intros. unfold SlowMorph.
+  destruct (CR_complete R2 _
+       (CRmorph_rat_cv _
+          (Rcv_cauchy_mod
+             (fun n : nat => CR_of_Q R1 (let (q0, _) := CR_Q_limit (CR_of_Q R1 q) n in q0))
+             (CR_of_Q R1 q) (CR_Q_limit_cv (CR_of_Q R1 q))))).
+  apply (CR_cv_unique _ _ _ c).
+  intro p. exists (Pos.to_nat p). intros.
+  destruct (CR_Q_limit (CR_of_Q R1 q) i). rewrite CRabs_right.
+  apply (CRplus_le_reg_r (CR_of_Q R2 q)). unfold CRminus.
+  rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r, CRplus_comm.
+  rewrite <- CR_of_Q_plus. apply CR_of_Q_le.
+  destruct (Q_dec x0 (q + (1 # p))%Q). destruct s.
+  apply Qlt_le_weak, q0. exfalso. pose proof (CR_of_Q_lt R1 _ _ q0).
+  apply (CRlt_asym _ _ H0). apply (CRlt_le_trans _ _ _ (snd p0)). clear H0.
+  rewrite <- CR_of_Q_plus. apply CR_of_Q_le. apply Qplus_le_r.
+  unfold Qle, Qnum, Qden. rewrite Z.mul_1_l, Z.mul_1_l.
+  apply Pos2Z.pos_le_pos, Pos2Nat.inj_le. rewrite Nat2Pos.id. exact H.
+  destruct i. exfalso. inversion H. pose proof (Pos2Nat.is_pos p).
+  rewrite H1 in H0. inversion H0. discriminate.
+  rewrite q0. apply Qle_refl.
+  rewrite <- (CRplus_opp_r (CR_of_Q R2 q)). apply CRplus_le_compat_r, CR_of_Q_le.
+  destruct (Q_dec q x0). destruct s. apply Qlt_le_weak, q0.
+  exfalso. apply (CRlt_asym _ _ (fst p0)). apply CR_of_Q_lt. exact q0.
+  rewrite q0. apply Qle_refl.
+Qed.
+
+(* The increasing property of morphisms, when the left bound is rational. *)
+Lemma SlowMorph_increasing_Qr
+  : forall {R1 R2 : ConstructiveReals} (x : CRcarrier R1) (q : Q),
+    CR_of_Q R1 q < x -> CR_of_Q R2 q < SlowMorph x.
+Proof.
+  intros.
+  unfold SlowMorph;
+  destruct (CR_complete R2 _
+       (CRmorph_rat_cv _
+          (Rcv_cauchy_mod (fun n : nat => CR_of_Q R1 (let (q0, _) := CR_Q_limit x n in q0)) x
+             (CR_Q_limit_cv x)))).
+  destruct (CR_Q_dense R1 _ _ H) as [r [H0 H1]].
+  apply lt_CR_of_Q in H0.
+  apply (CRlt_le_trans _ (CR_of_Q R2 r)).
+  apply CR_of_Q_lt, H0.
+  assert (forall n:nat, le O n -> CR_of_Q R2 r <= CR_of_Q R2 (let (q0, _) := CR_Q_limit x n in q0)).
+  { intros. apply CR_of_Q_le. destruct (CR_Q_limit x n).
+    destruct (Q_dec r x1). destruct s. apply Qlt_le_weak, q0.
+    exfalso. apply (CR_of_Q_lt R1) in q0.
+    apply (CRlt_asym _ _ q0). exact (CRlt_trans _ _ _ H1 (fst p)).
+    rewrite q0. apply Qle_refl. }
+  exact (CR_cv_bound_down _ _ _ O H2 c).
+Qed.
+
+(* The increasing property of morphisms, when the right bound is rational. *)
+Lemma SlowMorph_increasing_Ql
+  : forall {R1 R2 : ConstructiveReals} (x : CRcarrier R1) (q : Q),
+    x < CR_of_Q R1 q -> SlowMorph x < CR_of_Q R2 q.
+Proof.
+  intros.
+  unfold SlowMorph;
+  destruct (CR_complete R2 _
+       (CRmorph_rat_cv _
+          (Rcv_cauchy_mod (fun n : nat => CR_of_Q R1 (let (q0, _) := CR_Q_limit x n in q0)) x
+             (CR_Q_limit_cv x)))).
+  assert (CR_cv R1 (fun n => CR_of_Q R1 (let (q0, _) := CR_Q_limit x n in q0)
+                             + CR_of_Q R1 (1 # Pos.of_nat n)) x).
+  { apply (CR_cv_proper _ (x+0)). apply CR_cv_plus. apply CR_Q_limit_cv.
+    intro p. exists (Pos.to_nat p). intros.
+    unfold CRminus. rewrite CRopp_0, CRplus_0_r. rewrite CRabs_right.
+    apply CR_of_Q_le. unfold Qle, Qnum, Qden. do 2 rewrite Z.mul_1_l.
+    apply Pos2Z.pos_le_pos, Pos2Nat.inj_le. rewrite Nat2Pos.id. exact H0.
+    destruct i. inversion H0. pose proof (Pos2Nat.is_pos p).
+    rewrite H2 in H1. inversion H1. discriminate.
+    rewrite <- CR_of_Q_zero. apply CR_of_Q_le. discriminate.
+    rewrite CRplus_0_r. reflexivity. }
+  pose proof (CR_cv_open_above _ _ _ H0 H) as [n nmaj].
+  apply (CRle_lt_trans _ (CR_of_Q R2 (let (q0, _) := CR_Q_limit x n in
+                                      q0 + (1 # Pos.of_nat n)))).
+  - apply (CR_cv_bound_up (fun n : nat => CR_of_Q R2 (let (q0, _) := CR_Q_limit x n in q0)) _ _ n).
+    2: exact c. intros. destruct (CR_Q_limit x n0), (CR_Q_limit x n).
+    apply CR_of_Q_le, Qlt_le_weak. apply (lt_CR_of_Q R1).
+    apply (CRlt_le_trans _ _ _ (snd p)).
+    apply (CRle_trans _ (CR_of_Q R1 x2 + CR_of_Q R1 (1 # Pos.of_nat n0))).
+    apply CRplus_le_compat_r. apply CRlt_asym, p0.
+    rewrite <- CR_of_Q_plus. apply CR_of_Q_le. apply Qplus_le_r.
+    unfold Qle, Qnum, Qden. do 2 rewrite Z.mul_1_l.
+    apply Pos2Z.pos_le_pos, Pos2Nat.inj_le.
+    destruct n. destruct n0. apply le_refl.
+    rewrite (Nat2Pos.id (S n0)). apply le_n_S, le_0_n. discriminate.
+    destruct n0. exfalso; inversion H1.
+    rewrite Nat2Pos.id, Nat2Pos.id. exact H1. discriminate. discriminate.
+  - specialize (nmaj n (le_refl n)).
+    destruct (CR_Q_limit x n). apply CR_of_Q_lt.
+    rewrite <- CR_of_Q_plus in nmaj. apply lt_CR_of_Q in nmaj. exact nmaj.
+Qed.
+
+Lemma SlowMorph_increasing : forall {R1 R2 : ConstructiveReals} (x y : CRcarrier R1),
+    x < y -> @SlowMorph R1 R2 x < SlowMorph y.
+Proof.
+  intros.
+  destruct (CR_Q_dense R1 _ _ H) as [q [H0 H1]].
+  apply (CRlt_trans _ (CR_of_Q R2 q)).
+  apply SlowMorph_increasing_Ql. exact H0.
+  apply SlowMorph_increasing_Qr. exact H1.
+Qed.
+
+
+(* We call this morphism slow to remind that it should only be used
+   for proofs, not for computations. *)
+Definition SlowConstructiveRealsMorphism {R1 R2 : ConstructiveReals}
+  : @ConstructiveRealsMorphism R1 R2
+  := Build_ConstructiveRealsMorphism
+       R1 R2 SlowMorph CauchyMorph_rat
+       SlowMorph_increasing.
+
+Lemma CRmorph_abs : forall {R1 R2 : ConstructiveReals}
+                      (f : @ConstructiveRealsMorphism R1 R2)
+                      (x : CRcarrier R1),
+    CRabs R2 (CRmorph f x) == CRmorph f (CRabs R1 x).
+Proof.
+  assert (forall {R1 R2 : ConstructiveReals}
+            (f : @ConstructiveRealsMorphism R1 R2)
+            (x : CRcarrier R1),
+             CRabs R2 (CRmorph f x) <= CRmorph f (CRabs R1 x)).
+  { intros. rewrite <- CRabs_def. split.
+    - apply CRmorph_le.
+      pose proof (CRabs_def _ x (CRabs R1 x)) as [_ H].
+      apply H, CRle_refl.
+    - apply (CRle_trans _ (CRmorph f (CRopp R1 x))).
+      apply CRmorph_opp. apply CRmorph_le.
+      pose proof (CRabs_def _ x (CRabs R1 x)) as [_ H].
+      apply H, CRle_refl. }
+  intros. split. 2: apply H.
+  apply (CRmorph_le_inv (@SlowConstructiveRealsMorphism R2 R1)).
+  apply (CRle_trans _ (CRabs R1 x)).
+  apply (Endomorph_id
+           (CRmorph_compose f (@SlowConstructiveRealsMorphism R2 R1))).
+  apply (CRle_trans
+           _ (CRabs R1 (CRmorph (@SlowConstructiveRealsMorphism R2 R1) (CRmorph f x)))).
+  apply CRabs_morph.
+  apply CReq_sym, (Endomorph_id
+                      (CRmorph_compose f (@SlowConstructiveRealsMorphism R2 R1))).
+  apply H.
+Qed.
+
+Lemma CRmorph_cv : forall {R1 R2 : ConstructiveReals}
+                     (f : @ConstructiveRealsMorphism R1 R2)
+                     (un : nat -> CRcarrier R1)
+                     (l : CRcarrier R1),
+    CR_cv R1 un l
+    -> CR_cv R2 (fun n => CRmorph f (un n)) (CRmorph f l).
+Proof.
+  intros. intro p. specialize (H p) as [n H].
+  exists n. intros. specialize (H i H0).
+  unfold CRminus. rewrite <- CRmorph_opp, <- CRmorph_plus, CRmorph_abs.
+  rewrite <- (CRmorph_rat f (1#p)). apply CRmorph_le. exact H.
+Qed.
+
+Lemma CRmorph_cauchy_reverse : forall {R1 R2 : ConstructiveReals}
+                     (f : @ConstructiveRealsMorphism R1 R2)
+                     (un : nat -> CRcarrier R1),
+    CR_cauchy R2 (fun n => CRmorph f (un n))
+    -> CR_cauchy R1 un.
+Proof.
+  intros. intro p. specialize (H p) as [n H].
+  exists n. intros. specialize (H i j H0 H1).
+  unfold CRminus in H. rewrite <- CRmorph_opp, <- CRmorph_plus, CRmorph_abs in H.
+  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
new file mode 100644
index 0000000000..11c8e5d8a2
--- /dev/null
+++ b/theories/Reals/Abstract/ConstructiveSum.v
@@ -0,0 +1,348 @@
+(************************************************************************)
+(*         *   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 ConstructiveAbs.
+
+Local Open Scope ConstructiveReals.
+
+
+(**
+   Definition and properties of finite sums and powers.
+*)
+
+Fixpoint CRsum {R : ConstructiveReals}
+         (f:nat -> CRcarrier R) (N:nat) : CRcarrier R :=
+  match N with
+    | O => f 0%nat
+    | 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) ->
+    CRsum An N == CRsum Bn N.
+Proof.
+  induction N.
+  - intros. exact (H O (le_refl _)).
+  - intros. simpl. apply CRplus_morph. apply IHN.
+    intros. apply H. apply (le_trans _ N _ H0), le_S, le_refl.
+    apply H, le_refl.
+Qed.
+
+Lemma sum_eq_R0 : forall {R : ConstructiveReals} (un : nat -> CRcarrier R) (n : nat),
+    (forall k:nat, un k == 0)
+    -> CRsum un n == 0.
+Proof.
+  induction n.
+  - intros. apply H.
+  - intros. simpl. rewrite IHn. rewrite H. apply CRplus_0_l. exact H.
+Qed.
+
+Definition INR {R : ConstructiveReals} (n : nat) : CRcarrier R
+  := CR_of_Q R (Z.of_nat n # 1).
+
+Lemma sum_const : forall {R : ConstructiveReals} (a : CRcarrier R) (n : nat),
+    CRsum (fun _ => a) n == a * INR (S n).
+Proof.
+  induction n.
+  - unfold INR. simpl. rewrite CR_of_Q_one, CRmult_1_r. reflexivity.
+  - simpl. rewrite IHn. unfold INR.
+    replace (Z.of_nat (S (S n))) with (Z.of_nat (S n) + 1)%Z.
+    rewrite <- Qinv_plus_distr, CR_of_Q_plus, CRmult_plus_distr_l.
+    apply CRplus_morph. reflexivity. rewrite CR_of_Q_one, CRmult_1_r. reflexivity.
+    replace 1%Z with (Z.of_nat 1). rewrite <- Nat2Z.inj_add.
+    apply f_equal. rewrite Nat.add_comm. reflexivity. reflexivity.
+Qed.
+
+Lemma multiTriangleIneg : forall {R : ConstructiveReals} (u : nat -> CRcarrier R) (n : nat),
+    CRabs R (CRsum u n) <= CRsum (fun k => CRabs R (u k)) n.
+Proof.
+  induction n.
+  - apply CRle_refl.
+  - simpl. apply (CRle_trans _ (CRabs R (CRsum u n) + CRabs R (u (S n)))).
+    apply CRabs_triang. apply CRplus_le_compat. apply IHn.
+    apply CRle_refl.
+Qed.
+
+Lemma sum_assoc : forall {R : ConstructiveReals} (u : nat -> CRcarrier R) (n p : nat),
+    CRsum u (S n + p)
+    == CRsum u n + CRsum (fun k => u (S n + k)%nat) p.
+Proof.
+  induction p.
+  - simpl. rewrite Nat.add_0_r. reflexivity.
+  - simpl. rewrite (Radd_assoc (CRisRing R)). apply CRplus_morph.
+    rewrite Nat.add_succ_r.
+    rewrite (CRsum_eq (fun k : nat => u (S (n + k))) (fun k : nat => u (S n + k)%nat)).
+    rewrite <- IHp. reflexivity. intros. reflexivity. reflexivity.
+Qed.
+
+Lemma sum_Rle : forall {R : ConstructiveReals} (un vn : nat -> CRcarrier R) (n : nat),
+    (forall k, le k n -> un k <= vn k)
+    -> CRsum un n <= CRsum vn n.
+Proof.
+  induction n.
+  - intros. apply H. apply le_refl.
+  - intros. simpl. apply CRplus_le_compat. apply IHn.
+    intros. apply H. apply (le_trans _ n _ H0). apply le_S, le_refl.
+    apply H. apply le_refl.
+Qed.
+
+Lemma Abs_sum_maj : forall {R : ConstructiveReals} (un vn : nat -> CRcarrier R),
+    (forall n:nat, CRabs R (un n) <= (vn n))
+    -> forall n p:nat, (CRabs R (CRsum un n - CRsum un p) <=
+              CRsum vn (Init.Nat.max n p) - CRsum vn (Init.Nat.min n p)).
+Proof.
+  intros. destruct (le_lt_dec n p).
+  - destruct (Nat.le_exists_sub n p) as [k [maj _]]. assumption.
+    subst p. rewrite max_r. rewrite min_l.
+    setoid_replace (CRsum un n - CRsum un (k + n))
+      with (-(CRsum un (k + n) - CRsum un n)).
+    rewrite CRabs_opp.
+    destruct k. simpl. unfold CRminus. rewrite CRplus_opp_r.
+    rewrite CRplus_opp_r. rewrite CRabs_right.
+    apply CRle_refl. apply CRle_refl.
+    replace (S k + n)%nat with (S n + k)%nat.
+    unfold CRminus. rewrite sum_assoc. rewrite sum_assoc.
+    rewrite CRplus_comm.
+    rewrite <- CRplus_assoc. rewrite CRplus_opp_l.
+    rewrite CRplus_0_l. rewrite CRplus_comm.
+    rewrite <- CRplus_assoc. rewrite CRplus_opp_l.
+    rewrite CRplus_0_l.
+    apply (CRle_trans _ (CRsum (fun k0 : nat => CRabs R (un (S n + k0)%nat)) k)).
+    apply multiTriangleIneg. apply sum_Rle. intros.
+    apply H. rewrite Nat.add_comm, Nat.add_succ_r. reflexivity.
+    unfold CRminus. rewrite CRopp_plus_distr, CRopp_involutive, CRplus_comm.
+    reflexivity. assumption. assumption.
+  - destruct (Nat.le_exists_sub p n) as [k [maj _]]. unfold lt in l.
+    apply (le_trans p (S p)). apply le_S. apply le_refl. assumption.
+    subst n. rewrite max_l. rewrite min_r.
+    destruct k. simpl. unfold CRminus. rewrite CRplus_opp_r.
+    rewrite CRplus_opp_r. rewrite CRabs_right. apply CRle_refl.
+    apply CRle_refl.
+    replace (S k + p)%nat with (S p + k)%nat. unfold CRminus.
+    rewrite sum_assoc. rewrite sum_assoc.
+    rewrite CRplus_comm.
+    rewrite <- CRplus_assoc. rewrite CRplus_opp_l.
+    rewrite CRplus_0_l. rewrite CRplus_comm.
+    rewrite <- CRplus_assoc. rewrite CRplus_opp_l.
+    rewrite CRplus_0_l.
+    apply (CRle_trans _ (CRsum (fun k0 : nat => CRabs R (un (S p + k0)%nat)) k)).
+    apply multiTriangleIneg. apply sum_Rle. intros.
+    apply H. rewrite Nat.add_comm, Nat.add_succ_r. reflexivity.
+    apply (le_trans p (S p)). apply le_S. apply le_refl. assumption.
+    apply (le_trans p (S p)). apply le_S. apply le_refl. assumption.
+Qed.
+
+Lemma cond_pos_sum : forall {R : ConstructiveReals} (un : nat -> CRcarrier R) (n : nat),
+    (forall k, 0 <= un k)
+    -> 0 <= CRsum un n.
+Proof.
+  induction n.
+  - intros. apply H.
+  - intros. simpl. rewrite <- CRplus_0_r.
+    apply CRplus_le_compat. apply IHn, H. apply H.
+Qed.
+
+Lemma pos_sum_more : forall {R : ConstructiveReals} (u : nat -> CRcarrier R)
+                       (n p : nat),
+    (forall k:nat, 0 <= u k)
+    -> le n p -> CRsum u n <= CRsum u p.
+Proof.
+  intros. destruct (Nat.le_exists_sub n p H0). destruct H1. subst p.
+  rewrite plus_comm.
+  destruct x. rewrite plus_0_r. apply CRle_refl. rewrite Nat.add_succ_r.
+  replace (S (n + x)) with (S n + x)%nat. rewrite sum_assoc.
+  rewrite <- CRplus_0_r, CRplus_assoc.
+  apply CRplus_le_compat_l. rewrite CRplus_0_l.
+  apply cond_pos_sum.
+  intros. apply H. auto.
+Qed.
+
+Lemma sum_opp : forall {R : ConstructiveReals} (un : nat -> CRcarrier R) (n : nat),
+    CRsum (fun k => - un k) n == - CRsum un n.
+Proof.
+  induction n.
+  - reflexivity.
+  - simpl. rewrite IHn. rewrite CRopp_plus_distr. reflexivity.
+Qed.
+
+Lemma sum_scale : forall {R : ConstructiveReals} (u : nat -> CRcarrier R) (a : CRcarrier R) (n : nat),
+    CRsum (fun k : nat => u k * a) n == CRsum u n * a.
+Proof.
+  induction n.
+  - simpl. rewrite (Rmul_comm (CRisRing R)). reflexivity.
+  - simpl. rewrite IHn. rewrite CRmult_plus_distr_r.
+    apply CRplus_morph. reflexivity.
+    rewrite (Rmul_comm (CRisRing R)). reflexivity.
+Qed.
+
+Lemma sum_plus : forall {R : ConstructiveReals} (u v : nat -> CRcarrier R) (n : nat),
+    CRsum (fun n0 : nat => u n0 + v n0) n == CRsum u n + CRsum v n.
+Proof.
+  induction n.
+  - reflexivity.
+  - simpl. rewrite IHn. do 2 rewrite CRplus_assoc.
+    apply CRplus_morph. reflexivity. rewrite CRplus_comm, CRplus_assoc.
+    apply CRplus_morph. reflexivity. apply CRplus_comm.
+Qed.
+
+Lemma decomp_sum :
+  forall {R : ConstructiveReals} (An:nat -> CRcarrier R) (N:nat),
+    (0 < N)%nat ->
+    CRsum An N == An 0%nat + CRsum (fun i:nat => An (S i)) (pred N).
+Proof.
+  induction N.
+  - intros. exfalso. inversion H.
+  - intros _. destruct N. simpl. reflexivity. simpl.
+    rewrite IHN. rewrite CRplus_assoc.
+    apply CRplus_morph. reflexivity. reflexivity.
+    apply le_n_S, le_0_n.
+Qed.
+
+Lemma reverse_sum : forall {R : ConstructiveReals} (u : nat -> CRcarrier R) (n : nat),
+    CRsum u n == CRsum (fun k => u (n-k)%nat) n.
+Proof.
+  induction n.
+  - intros. reflexivity.
+  - rewrite (decomp_sum (fun k : nat => u (S n - k)%nat)). simpl.
+    rewrite CRplus_comm. apply CRplus_morph. reflexivity. assumption.
+    unfold lt. apply le_n_S. apply le_0_n.
+Qed.
+
+Lemma Rplus_le_pos : forall {R : ConstructiveReals} (a b : CRcarrier R),
+    0 <= b -> a <= a + b.
+Proof.
+  intros. rewrite <- (CRplus_0_r a). rewrite CRplus_assoc.
+  apply CRplus_le_compat_l. rewrite CRplus_0_l. assumption.
+Qed.
+
+Lemma selectOneInSum : forall {R : ConstructiveReals} (u : nat -> CRcarrier R) (n i : nat),
+    le i n
+    -> (forall k:nat, 0 <= u k)
+    -> u i <= CRsum u n.
+Proof.
+  induction n.
+  - intros. inversion H. subst i. apply CRle_refl.
+  - intros. apply Nat.le_succ_r in H. destruct H.
+    apply (CRle_trans _ (CRsum u n)). apply IHn. assumption. assumption.
+    simpl. apply Rplus_le_pos. apply H0.
+    subst i. simpl. rewrite CRplus_comm. apply Rplus_le_pos.
+    apply cond_pos_sum. intros. apply H0.
+Qed.
+
+Lemma splitSum : forall {R : ConstructiveReals} (un : nat -> CRcarrier R)
+                        (filter : nat -> bool) (n : nat),
+    CRsum un n
+    == CRsum (fun i => if filter i then un i else 0) n
+       + CRsum (fun i => if filter i then 0 else un i) n.
+Proof.
+  induction n.
+  - simpl. destruct (filter O). symmetry; apply CRplus_0_r.
+    symmetry. apply CRplus_0_l.
+  - simpl. rewrite IHn. clear IHn. destruct (filter (S n)).
+    do 2 rewrite CRplus_assoc. apply CRplus_morph. reflexivity.
+    rewrite CRplus_comm. apply CRplus_morph. reflexivity. rewrite CRplus_0_r.
+    reflexivity. rewrite CRplus_0_r. rewrite CRplus_assoc. reflexivity.
+Qed.
+
+
+(* Power *)
+
+Lemma pow_R1_Rle : 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 pow_le : 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 pow_lt : 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 pow_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 pow_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 pow_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 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)).
+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.
+Qed.
+
+Lemma pow_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.