Replace classical reals quotient axioms by functional extensionality. Define homotopy propositions and homotopy sets. Rename local variable R in test Nsatz, to avoid a name collision with the type of real numbers.

13 files changed, 1021 insertions, 3081 deletions

diff --git a/doc/changelog/10-standard-library/10827-dedekind-reals.rst b/doc/changelog/10-standard-library/10827-dedekind-reals.rst
new file mode 100644
index 0000000000..5d8467025b
--- /dev/null
+++ b/doc/changelog/10-standard-library/10827-dedekind-reals.rst
@@ -0,0 +1,11 @@
+- New module `Reals.ClassicalDedekindReals` defines Dedekind real numbers
+  as boolean-values functions along with 3 logical axioms: limited principle
+  of omniscience, excluded middle of negations and functional extensionality.
+  The exposed type :g:`R` in module :g:`Reals.Rdefinitions` is those
+  Dedekind reals, hidden behind an opaque module.
+  Classical Dedekind reals are a quotient of constructive reals, which allows
+  to transport many constructive proofs to the classical case.
+
+  See `#10827 <https://github.com/coq/coq/pull/10827>`_, by Vincent Semeria,
+  based on discussions with Guillaume Melquiond, Bas Spitters and Hugo Herbelin,
+  code review by Hugo Herbelin.
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index d1b98b94a3..df7cda9aad 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -68,6 +68,7 @@ through the <tt>Require Import</tt> command.</p>
     theories/Logic/WKL.v
     theories/Logic/FinFun.v
     theories/Logic/PropFacts.v
+    theories/Logic/HLevels.v
   </dd>
 
   <dt> <b>Structures</b>:
@@ -518,8 +519,8 @@ through the <tt>Require Import</tt> command.</p>
     theories/Reals/ConstructiveRealsMorphisms.v
     theories/Reals/ConstructiveCauchyReals.v
     theories/Reals/ConstructiveCauchyRealsMult.v
+    theories/Reals/ClassicalDedekindReals.v
     theories/Reals/Raxioms.v
-    theories/Reals/ConstructiveRIneq.v
     theories/Reals/ConstructiveRealsLUB.v
     theories/Reals/RIneq.v
     theories/Reals/DiscrR.v
diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
index 66db924051..70c1077106 100644
--- a/plugins/syntax/r_syntax.ml
+++ b/plugins/syntax/r_syntax.ml
@@ -102,7 +102,7 @@ let bigint_of_z c = match DAst.get c with
 let rdefinitions = ["Coq";"Reals";"Rdefinitions"]
 let r_modpath = MPfile (make_dir rdefinitions)
 let r_base_modpath = MPdot (r_modpath, Label.make "RbaseSymbolsImpl")
-let r_path = make_path rdefinitions "R"
+let r_path = make_path ["Coq";"Reals";"Rdefinitions";"RbaseSymbolsImpl"] "R"
 
 let glob_IZR = GlobRef.ConstRef (Constant.make2 r_modpath @@ Label.make "IZR")
 let glob_Rmult = GlobRef.ConstRef (Constant.make2 r_base_modpath @@ Label.make "Rmult")
diff --git a/test-suite/success/Nsatz.v b/test-suite/success/Nsatz.v
index 381fbabe72..998f3f7dd1 100644
--- a/test-suite/success/Nsatz.v
+++ b/test-suite/success/Nsatz.v
@@ -419,13 +419,13 @@ Qed.
 
 
 
-Lemma Desargues: forall A B C A1 B1 C1 P Q R S:point,
+Lemma Desargues: forall A B C A1 B1 C1 P Q T S:point,
   X S = 0 -> Y S = 0 -> Y A = 0 ->
   collinear A S A1 -> collinear B S B1 -> collinear C S C1 ->
   collinear B1 C1 P -> collinear B C P ->
   collinear A1 C1 Q -> collinear A C Q -> 
-  collinear A1 B1 R -> collinear A B R ->
-  collinear P Q R
+  collinear A1 B1 T -> collinear A B T ->
+  collinear P Q T
   \/ X A = X B \/ X A = X C \/ X B = X C  \/ X A = 0 \/ Y B = 0 \/ Y C = 0
   \/ collinear S B C \/ parallel A C A1 C1 \/ parallel A B A1 B1.
 Proof.
@@ -440,8 +440,8 @@ let lv := rev (X A
              :: Y A1 :: X A1
                 :: Y B1
                    :: Y C1
-                      :: X R
-                         :: Y R
+                      :: X T
+                         :: Y T
                             :: X Q
                                :: Y Q :: X P :: Y P :: X C1 :: X B1 :: nil) in
 nsatz with radicalmax :=1%N strategy:=0%Z
diff --git a/theories/Logic/HLevels.v b/theories/Logic/HLevels.v
new file mode 100644
index 0000000000..010c4aad6f
--- /dev/null
+++ b/theories/Logic/HLevels.v
@@ -0,0 +1,146 @@
+(************************************************************************)
+(*         *   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)         *)
+(************************************************************************)
+
+(** The first three levels of homotopy type theory: homotopy propositions,
+    homotopy sets and homotopy one types. For more information,
+    https://github.com/HoTT/HoTT
+    and
+    https://homotopytypetheory.org/book
+
+    Univalence is not assumed here, and equality is Coq's usual inductive
+    type eq in sort Prop. This is a little different from HoTT, where
+    sort Prop does not exist and equality is directly in sort Type. *)
+
+
+(* It is almost impossible to prove that a type is a homotopy proposition
+   without funext, so we assume it here. *)
+Require Import Coq.Logic.FunctionalExtensionality.
+
+(* A homotopy proposition is a type that has at most one element.
+   Its unique inhabitant, when it exists, is to be interpreted as the
+   proof of the homotopy proposition.
+   Homotopy propositions are therefore an alternative to the sort Prop,
+   to select which types represent mathematical propositions. *)
+Definition IsHProp (P : Type) : Prop
+  := forall p q : P, p = q.
+
+(* A homotopy set is a type such as each equality type x = y is a
+   homotopy proposition. For example, any type which equality is
+   decidable in sort Prop is a homotopy set, as shown in file
+   Coq.Logic.Eqdep_dec.v. *)
+Definition IsHSet (X : Type) : Prop
+  := forall (x y : X) (p q : x = y), p = q.
+
+Definition IsHOneType (X : Type) : Prop
+  := forall (x y : X) (p q : x = y) (r s : p = q), r = s.
+
+Lemma forall_hprop : forall (A : Type) (P : A -> Prop),
+    (forall x:A, IsHProp (P x))
+    -> IsHProp (forall x:A, P x).
+Proof.
+  intros A P H p q. apply functional_extensionality_dep.
+  intro x. apply H.
+Qed.
+
+(* Homotopy propositions are stable by conjunction, but not by disjunction,
+   which can have a proof by the left and another proof by the right. *)
+Lemma and_hprop : forall P Q : Prop,
+    IsHProp P -> IsHProp Q -> IsHProp (P /\ Q).
+Proof.
+  intros. intros p q. destruct p,q.
+  replace p0 with p. replace q0 with q. reflexivity.
+  apply H0. apply H.
+Qed.
+
+Lemma impl_hprop : forall P Q : Prop,
+    IsHProp Q -> IsHProp (P -> Q).
+Proof.
+  intros P Q H p q. apply functional_extensionality.
+  intros. apply H.
+Qed.
+
+Lemma false_hprop : IsHProp False.
+Proof.
+  intros p q. contradiction.
+Qed.
+
+Lemma true_hprop : IsHProp True.
+Proof.
+  intros p q. destruct p,q. reflexivity.
+Qed.
+
+(* All negations are homotopy propositions. *)
+Lemma not_hprop : forall P : Type, IsHProp (P -> False).
+Proof.
+  intros P p q. apply functional_extensionality.
+  intros. contradiction.
+Qed.
+
+(* Homotopy propositions are included in homotopy sets.
+   They are the first 2 levels of a cumulative hierarchy of types
+   indexed by the natural numbers. In homotopy type theory,
+   homotopy propositions are call (-1)-types and homotopy
+   sets 0-types. *)
+Lemma hset_hprop : forall X : Type,
+    IsHProp X -> IsHSet X.
+Proof.
+  intros X H.
+  assert (forall (x y z:X) (p : y = z), eq_trans (H x y) p = H x z).
+  { intros. unfold eq_trans, eq_ind. destruct p. reflexivity. }
+  assert (forall (x y z:X) (p : y = z),
+             p = eq_trans (eq_sym (H x y)) (H x z)).
+  { intros. rewrite <- (H0 x y z p). unfold eq_trans, eq_sym, eq_ind.
+    destruct p, (H x y). reflexivity. }
+  intros x y p q.
+  rewrite (H1 x x y p), (H1 x x y q). reflexivity.
+Qed.
+
+Lemma eq_trans_cancel : forall {X : Type} {x y z : X} (p : x = y) (q r : y = z),
+  (eq_trans p q = eq_trans p r) -> q = r.
+Proof.
+  intros. destruct p. simpl in H. destruct r.
+  simpl in H. rewrite eq_trans_refl_l in H. exact H.
+Qed.
+
+Lemma hset_hOneType : forall X : Type,
+    IsHSet X -> IsHOneType X.
+Proof.
+  intros X f x y p q.
+  pose (fun a => f x y p a) as g.
+  assert (forall a (r : q = a), eq_trans (g q) r = g a).
+  { intros. destruct a. subst q. reflexivity. }
+  intros r s. pose proof (H p (eq_sym r)).
+  pose proof (H p (eq_sym s)).
+  rewrite <- H1 in H0. apply eq_trans_cancel in H0.
+  rewrite <- eq_sym_involutive. rewrite <- (eq_sym_involutive r).
+  rewrite H0. reflexivity.
+Qed.
+
+(* "IsHProp X" sounds like a proposition, because it asserts
+   a property of the type X. And indeed: *)
+Lemma hprop_hprop : forall X : Type,
+    IsHProp (IsHProp X).
+Proof.
+  intros X p q.
+  apply forall_hprop. intro x.
+  apply forall_hprop. intro y. intros f g.
+  apply (hset_hprop X p).
+Qed.
+
+Lemma hprop_hset : forall X : Type,
+    IsHProp (IsHSet X).
+Proof.
+  intros X f g.
+  apply functional_extensionality_dep. intro x.
+  apply functional_extensionality_dep. intro y.
+  apply functional_extensionality_dep. intro a.
+  apply functional_extensionality_dep. intro b.
+  apply (hset_hOneType). exact f.
+Qed.
diff --git a/theories/Reals/ClassicalDedekindReals.v b/theories/Reals/ClassicalDedekindReals.v
new file mode 100644
index 0000000000..e32def29b8
--- /dev/null
+++ b/theories/Reals/ClassicalDedekindReals.v
@@ -0,0 +1,465 @@
+(************************************************************************)
+(*         *   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 Coq.Logic.Eqdep_dec.
+Require Import Coq.Logic.FunctionalExtensionality.
+Require Import Coq.Logic.HLevels.
+Require Import QArith.
+Require Import Qabs.
+Require Import ConstructiveCauchyReals.
+Require Import ConstructiveRcomplete.
+
+(**
+   Classical Dedekind reals. With the 3 logical axioms funext,
+   sig_forall_dec and sig_not_dec, the lower cuts defined as
+   functions Q -> bool have all the classical properties of the
+   real numbers.
+
+   We could prove operations and theorems about them directly,
+   but instead we notice that they are a quotient of the
+   constructive Cauchy reals, from which they inherit many properties.
+*)
+
+(* The limited principle of omniscience *)
+Axiom sig_forall_dec
+  : forall (P : nat -> Prop),
+    (forall n, {P n} + {~P n})
+    -> {n | ~P n} + {forall n, P n}.
+
+Axiom sig_not_dec : forall P : Prop, { ~~P } + { ~P }.
+
+(* Try to find a surjection CReal -> lower cuts. *)
+Definition isLowerCut (f : Q -> bool) : Prop
+  := (forall q r:Q, Qle q r -> f r = true -> f q = true) (* interval *)
+     /\ ~(forall q:Q, f q = true) (* avoid positive infinity *)
+     /\ ~(forall q:Q, f q = false) (* avoid negative infinity *)
+     (* openness, the cut contains rational numbers
+        strictly lower than a real number. *)
+     /\ (forall q:Q, f q = true -> ~(forall r:Q, Qle r q \/ f r = false)).
+
+Lemma isLowerCut_hprop : forall (f : Q -> bool),
+    IsHProp (isLowerCut f).
+Proof.
+  intro f. apply and_hprop.
+  2: apply and_hprop. 2: apply not_hprop.
+  2: apply and_hprop. 2: apply not_hprop.
+  - apply forall_hprop. intro x.
+    apply forall_hprop. intro y.
+    apply impl_hprop. apply impl_hprop.
+    intros p q. apply eq_proofs_unicity_on.
+    intro b. destruct (f x), b.
+    left. reflexivity. right. discriminate.
+    right. discriminate. left. reflexivity.
+  - apply forall_hprop. intro q. apply impl_hprop. apply not_hprop.
+Qed.
+
+Lemma lowerCutBelow : forall f : Q -> bool,
+    isLowerCut f -> { q : Q | f q = true }.
+Proof.
+  intros.
+  destruct (sig_forall_dec (fun n:nat => f (-(Z.of_nat n # 1))%Q = false)).
+  - intro n. destruct (f (-(Z.of_nat n # 1))%Q).
+    right. discriminate. left. reflexivity.
+  - destruct s. exists (-(Z.of_nat x # 1))%Q.
+    destruct (f (-(Z.of_nat x # 1))%Q).
+    reflexivity. exfalso. apply n. reflexivity.
+  - exfalso. destruct H, H0, H1. apply H1. intro q.
+    destruct (f q) eqn:des. 2: reflexivity. exfalso.
+    destruct (Qarchimedean (-q)) as [p pmaj].
+    rewrite <- (Qplus_lt_l _ _ (q-(Z.pos p # 1))) in pmaj.
+    ring_simplify in pmaj.
+    specialize (H (- (Z.pos p#1))%Q q).
+    specialize (e (Pos.to_nat p)).
+    rewrite positive_nat_Z in e. rewrite H in e. discriminate.
+    2: exact des. ring_simplify. apply Qlt_le_weak, pmaj.
+Qed.
+
+Lemma lowerCutAbove : forall f : Q -> bool,
+    isLowerCut f -> { q : Q | f q = false }.
+Proof.
+  intros.
+  destruct (sig_forall_dec (fun n => f (Z.of_nat n # 1)%Q = true)).
+  - intro n. destruct (f (Z.of_nat n # 1)%Q).
+    left. reflexivity. right. discriminate.
+  - destruct s. exists (Z.of_nat x # 1)%Q. destruct (f (Z.of_nat x # 1)%Q).
+    exfalso. apply n. reflexivity. reflexivity.
+  - exfalso. destruct H, H0, H1. apply H0. intro q.
+    destruct (Qarchimedean q) as [p pmaj].
+    apply (H q (Z.of_nat (Pos.to_nat p) # 1)%Q).
+    rewrite positive_nat_Z. apply Qlt_le_weak, pmaj. apply e.
+Qed.
+
+Definition DReal : Set
+  := { f : Q -> bool | isLowerCut f }.
+
+Fixpoint DRealQlim_rec (f : Q -> bool) (low : isLowerCut f) (n p : nat) { struct p }
+  : f (proj1_sig (lowerCutBelow f low) + (Z.of_nat p # Pos.of_nat (S n)))%Q = false
+    -> { q : Q | f q = true /\ f (q + (1 # Pos.of_nat (S n)))%Q = false }.
+Proof.
+  intros. destruct p.
+  - exfalso. destruct (lowerCutBelow f low); unfold proj1_sig in H.
+    destruct low. rewrite (H0 _ x) in H. discriminate. simpl.
+    apply (Qplus_le_l _ _ (-x)). ring_simplify. discriminate. exact e.
+  - destruct (f (proj1_sig (lowerCutBelow f low) + (Z.of_nat p # Pos.of_nat (S n)))%Q) eqn:des.
+    + exists (proj1_sig (lowerCutBelow f low) + (Z.of_nat p # Pos.of_nat (S n)))%Q.
+      split. exact des.
+      destruct (f (proj1_sig (lowerCutBelow f low)
+                   + (Z.of_nat p # Pos.of_nat (S n)) + (1 # Pos.of_nat (S n)))%Q) eqn:d.
+      2: reflexivity. exfalso.
+      destruct low.
+      rewrite (e _ (proj1_sig (lowerCutBelow f (conj e a)) + (Z.of_nat p # Pos.of_nat (S n)) + (1 # Pos.of_nat (S n))))%Q in H.
+      discriminate. 2: exact d. rewrite <- Qplus_assoc, Qplus_le_r.
+      rewrite Qinv_plus_distr.
+      replace (Z.of_nat p + 1)%Z with (Z.of_nat (S p))%Z. apply Qle_refl.
+      replace 1%Z with (Z.of_nat 1). rewrite <- (Nat2Z.inj_add p 1).
+      apply f_equal. rewrite Nat.add_comm. reflexivity. reflexivity.
+    + destruct (DRealQlim_rec f low n p des) as [q qmaj].
+      exists q. exact qmaj.
+Qed.
+
+Definition DRealQlim (x : DReal) (n : nat)
+  : { q : Q | proj1_sig x q = true /\ proj1_sig x (q + (1# Pos.of_nat (S n)))%Q = false }.
+Proof.
+  destruct x as [f low].
+  destruct (lowerCutAbove f low).
+  destruct (Qarchimedean (x - proj1_sig (lowerCutBelow f low))) as [p pmaj].
+  apply (DRealQlim_rec f low n ((S n) * Pos.to_nat p)).
+  destruct (lowerCutBelow f low); unfold proj1_sig; unfold proj1_sig in pmaj.
+  destruct (f (x0 + (Z.of_nat (S n * Pos.to_nat p) # Pos.of_nat (S n)))%Q) eqn:des.
+  2: reflexivity. exfalso. destruct low.
+  rewrite (H _ (x0 + (Z.of_nat (S n * Pos.to_nat p) # Pos.of_nat (S n)))%Q) in e.
+  discriminate. 2: exact des.
+  setoid_replace (Z.of_nat (S n * Pos.to_nat p) # Pos.of_nat (S n))%Q with (Z.pos p # 1)%Q.
+  apply (Qplus_lt_l _ _ x0) in pmaj. ring_simplify in pmaj.
+  apply Qlt_le_weak, pmaj. rewrite Nat2Z.inj_mul, positive_nat_Z.
+  unfold Qeq, Qnum, Qden. rewrite Z.mul_1_r, Z.mul_comm.
+  replace (Z.of_nat (S n)) with (Z.pos (Pos.of_nat (S n))). reflexivity.
+  simpl. destruct n. reflexivity. apply f_equal.
+  apply Pos.succ_of_nat. discriminate.
+Qed.
+
+Definition DRealAbstr : CReal -> DReal.
+Proof.
+  intro x.
+  assert (forall (q : Q) (n : nat),
+   {(fun n0 : nat => (proj1_sig x (S n0) <= q + (1 # Pos.of_nat (S n0)))%Q) n} +
+   {~ (fun n0 : nat => (proj1_sig x (S n0) <= q + (1 # Pos.of_nat (S n0)))%Q) n}).
+  { intros. destruct (Qlt_le_dec (q + (1 # Pos.of_nat (S n))) (proj1_sig x (S n))).
+    right. apply (Qlt_not_le _ _ q0). left. exact q0. }
+
+  exists (fun q:Q => if sig_forall_dec (fun n:nat => Qle (proj1_sig x (S n)) (q + (1#Pos.of_nat (S n)))) (H q)
+             then true else false).
+  repeat split.
+  - intros.
+    destruct (sig_forall_dec (fun n : nat => (proj1_sig x (S n) <= q + (1 # Pos.of_nat (S n)))%Q)
+                             (H q)).
+    reflexivity. exfalso.
+    destruct (sig_forall_dec (fun n : nat => (proj1_sig x (S n) <= r + (1 # Pos.of_nat (S n)))%Q)
+                             (H r)).
+    destruct s. apply n.
+    apply (Qle_trans _ _ _ (q0 x0)).
+    apply Qplus_le_l. exact H0. discriminate.
+  - intro abs. destruct (Rfloor x) as [z [_ zmaj]].
+    specialize (abs (z+3 # 1)%Q).
+    destruct (sig_forall_dec (fun n : nat => (proj1_sig x (S n) <= (z+3 # 1) + (1 # Pos.of_nat (S n)))%Q)
+                             (H (z+3 # 1)%Q)).
+    2: exfalso; discriminate. clear abs. destruct s as [n nmaj]. apply nmaj.
+    rewrite <- (inject_Q_plus (z#1) 2) in zmaj.
+    apply CRealLt_asym in zmaj. rewrite <- CRealLe_not_lt in zmaj.
+    specialize (zmaj (Pos.of_nat (S n))). unfold inject_Q, proj1_sig in zmaj.
+    rewrite Nat2Pos.id in zmaj. 2: discriminate.
+    destruct x as [xn xcau]; unfold proj1_sig.
+    rewrite Qinv_plus_distr in zmaj.
+    apply (Qplus_le_l _ _ (-(z + 2 # 1))). apply (Qle_trans _ _ _ zmaj).
+    apply (Qplus_le_l _ _ (-(1 # Pos.of_nat (S n)))). apply (Qle_trans _ 1).
+    unfold Qopp, Qnum, Qden. rewrite Qinv_plus_distr.
+    unfold Qle, Qnum, Qden. apply Z2Nat.inj_le. discriminate. discriminate.
+    do 2 rewrite Z.mul_1_l. unfold Z.to_nat. rewrite Nat2Pos.id. 2: discriminate.
+    apply le_n_S, le_0_n. setoid_replace (- (z + 2 # 1))%Q with (-(z+2) #1)%Q.
+    2: reflexivity. ring_simplify. rewrite Qinv_plus_distr.
+    replace (z + 3 + - (z + 2))%Z with 1%Z. apply Qle_refl. ring.
+  - intro abs. destruct (Rfloor x) as [z [zmaj _]].
+    specialize (abs (z-4 # 1)%Q).
+    destruct (sig_forall_dec (fun n : nat => (proj1_sig x (S n) <= (z-4 # 1) + (1 # Pos.of_nat (S n)))%Q)
+                             (H (z-4 # 1)%Q)).
+    exfalso; discriminate. clear abs.
+    apply CRealLt_asym in zmaj. apply zmaj. clear zmaj.
+    exists 1%positive. unfold inject_Q, proj1_sig.
+    specialize (q O).
+    destruct x as [xn xcau]; unfold proj1_sig; unfold proj1_sig in q.
+    unfold Pos.of_nat in q. rewrite Qinv_plus_distr in q.
+    unfold Pos.to_nat; simpl. apply (Qplus_lt_l _ _ (xn 1%nat - 2)).
+    ring_simplify. rewrite Qinv_plus_distr.
+    apply (Qle_lt_trans _ _ _ q). apply Qlt_minus_iff.
+    unfold Qopp, Qnum, Qden. rewrite Qinv_plus_distr.
+    replace (z + -2 + - (z - 4 + 1))%Z with 1%Z. 2: ring. reflexivity.
+  - intros q H0 abs.
+    destruct (sig_forall_dec (fun n : nat => (proj1_sig x (S n) <= q + (1 # Pos.of_nat (S n)))%Q) (H q)).
+    2: exfalso; discriminate. clear H0.
+    destruct x as [xn xcau]; unfold proj1_sig in abs, s.
+    destruct s as [n nmaj].
+    (* We have that q < x as real numbers. The middle
+       (q + xSn - 1/Sn)/2 is also lower than x, witnessed by the same index n. *)
+    specialize (abs ((q + xn (S n) - (1 # Pos.of_nat (S n))%Q)/2)%Q).
+    destruct abs.
+    + apply (Qmult_le_r _ _ 2) in H0. field_simplify in H0.
+      apply (Qplus_le_r _ _ ((1 # Pos.of_nat (S n)) - q)) in H0.
+      ring_simplify in H0. apply nmaj. rewrite Qplus_comm. exact H0. reflexivity.
+    + destruct (sig_forall_dec
+           (fun n0 : nat =>
+            (xn (S n0) <= (q + xn (S n) - (1 # Pos.of_nat (S n))) / 2 + (1 # Pos.of_nat (S n0)))%Q)
+           (H ((q + xn (S n) - (1 # Pos.of_nat (S n))) / 2)%Q)).
+      discriminate. clear H0. specialize (q0 n).
+      apply (Qmult_le_l _ _ 2) in q0. field_simplify in q0.
+      apply (Qplus_le_l _ _ (-xn (S n))) in q0. ring_simplify in q0.
+      contradiction. reflexivity.
+Defined.
+
+Lemma UpperAboveLower : forall (f : Q -> bool) (q r : Q),
+    isLowerCut f
+    -> f q = true
+    -> f r = false
+    -> Qlt q r.
+Proof.
+  intros. destruct H. apply Qnot_le_lt. intro abs.
+  rewrite (H r q abs) in H1. discriminate. exact H0.
+Qed.
+
+Definition DRealRepr : DReal -> CReal.
+Proof.
+  intro x. exists (fun n => proj1_sig (DRealQlim x n)).
+  intros n p q H H0.
+  destruct (DRealQlim x p), (DRealQlim x q); unfold proj1_sig.
+  destruct x as [f low]; unfold proj1_sig in a0, a.
+  apply Qabs_case.
+  - intros. apply (Qlt_le_trans _ (1 # Pos.of_nat (S q))).
+    apply (Qplus_lt_l _ _ x1). ring_simplify. apply (UpperAboveLower f).
+    exact low. apply a. apply a0. unfold Qle, Qnum, Qden.
+    do 2 rewrite Z.mul_1_l. apply Pos2Z.pos_le_pos.
+    apply Pos2Nat.inj_le. rewrite Nat2Pos.id. apply (le_trans _ _ _ H0), le_S, le_refl.
+    discriminate.
+  - intros. apply (Qlt_le_trans _ (1 # Pos.of_nat (S p))).
+    apply (Qplus_lt_l _ _ x0). ring_simplify. apply (UpperAboveLower f).
+    exact low. apply a0. apply a. unfold Qle, Qnum, Qden.
+    do 2 rewrite Z.mul_1_l. apply Pos2Z.pos_le_pos.
+    apply Pos2Nat.inj_le. rewrite Nat2Pos.id. apply (le_trans _ _ _ H), le_S, le_refl.
+    discriminate.
+Defined.
+
+Definition Rle (x y : DReal)
+  := forall q:Q, proj1_sig x q = true -> proj1_sig y q = true.
+
+Lemma Rle_antisym : forall x y : DReal,
+    Rle x y
+    -> Rle y x
+    -> x = y.
+Proof.
+  intros [f cf] [g cg] H H0. unfold Rle in H,H0; simpl in H, H0.
+  assert (f = g).
+  { apply functional_extensionality. intro q.
+    specialize (H q). specialize (H0 q).
+    destruct (f q), (g q). reflexivity.
+    exfalso. specialize (H (eq_refl _)). discriminate.
+    exfalso. specialize (H0 (eq_refl _)). discriminate.
+    reflexivity. }
+  subst g. replace cg with cf. reflexivity.
+  apply isLowerCut_hprop.
+Qed.
+
+Lemma lowerUpper : forall (f : Q -> bool) (q r : Q),
+    isLowerCut f -> Qle q r -> f q = false -> f r = false.
+Proof.
+  intros. destruct H. specialize (H q r H0). destruct (f r) eqn:desR.
+  2: reflexivity. exfalso. specialize (H (eq_refl _)).
+  rewrite H in H1. discriminate.
+Qed.
+
+Lemma DRealOpen : forall (x : DReal) (q : Q),
+    proj1_sig x q = true
+    -> { r : Q | Qlt q r /\ proj1_sig x r = true }.
+Proof.
+  intros.
+  destruct (sig_forall_dec (fun n => Qle (proj1_sig (DRealQlim x n)) q)).
+  - intro n. destruct (DRealQlim x n); unfold proj1_sig.
+    destruct (Qlt_le_dec q x0). right. exact (Qlt_not_le _ _ q0).
+    left. exact q0.
+  - destruct s. apply Qnot_le_lt in n.
+    destruct (DRealQlim x x0); unfold proj1_sig in n.
+    exists x1. split. exact n. apply a.
+  - exfalso. destruct x as [f low]. unfold proj1_sig in H, q0.
+    destruct low, a, a. apply (n1 q H). intros.
+    destruct (Qlt_le_dec q r). 2: left; exact q1. right.
+    destruct (Qarchimedean (/(r - q))) as [p pmaj].
+    specialize (q0 (Pos.to_nat p)).
+    destruct (DRealQlim (exist _ f (conj e (conj n (conj n0 n1)))) (Pos.to_nat p))
+      as [s smaj].
+    unfold proj1_sig in smaj.
+    apply (lowerUpper f (s + (1 # Pos.of_nat (S (Pos.to_nat p))))).
+    exact (conj e (conj n (conj n0 n1))).
+    2: apply smaj. apply (Qle_trans _ (s + (r-q))).
+    apply Qplus_le_r. apply (Qle_trans _ (1 # p)).
+    unfold Qle, Qnum, Qden. do 2 rewrite Z.mul_1_l.
+    apply Pos2Z.pos_le_pos. apply Pos2Nat.inj_le.
+    rewrite Nat2Pos.id. apply le_S, le_refl. discriminate.
+    apply (Qmult_le_l _ _ ( (Z.pos p # 1) / (r-q))).
+    rewrite <- (Qmult_0_r (Z.pos p #1)). apply Qmult_lt_l.
+    reflexivity. apply Qinv_lt_0_compat.
+    unfold Qminus. rewrite <- Qlt_minus_iff. exact q1.
+    unfold Qdiv. rewrite Qmult_comm, <- Qmult_assoc.
+    rewrite (Qmult_comm (/(r-q))), Qmult_inv_r, Qmult_assoc.
+    setoid_replace ((1 # p) * (Z.pos p # 1))%Q with 1%Q.
+    2: reflexivity. rewrite Qmult_1_l, Qmult_1_r.
+    apply Qlt_le_weak, pmaj. intro abs. apply Qlt_minus_iff in q1.
+    rewrite abs in q1. apply (Qlt_not_le _ _ q1), Qle_refl.
+    apply (Qplus_le_l _ _ (q-r)). ring_simplify. exact q0.
+Qed.
+
+Lemma DRealReprQ : forall (x : DReal) (q : Q),
+    proj1_sig x q = true
+    -> CRealLt (inject_Q q) (DRealRepr x).
+Proof.
+  intros.
+  destruct (DRealOpen x q H) as [r rmaj].
+  destruct (Qarchimedean (4/(r - q))) as [p pmaj].
+  exists p.
+  destruct x as [f low]; unfold DRealRepr, inject_Q, proj1_sig.
+  destruct (DRealQlim (exist _ f low) (Pos.to_nat p)) as [s smaj].
+  unfold proj1_sig in smaj, rmaj.
+  apply (Qplus_lt_l _ _ (q+ (1 # Pos.of_nat (S (Pos.to_nat p))))).
+  ring_simplify. rewrite <- (Qplus_comm s).
+  apply (UpperAboveLower f _ _ low). 2: apply smaj.
+  destruct low. apply (e _ r). 2: apply rmaj.
+  rewrite <- (Qplus_comm q).
+  apply (Qle_trans _ (q + (4#p))).
+  - rewrite <- Qplus_assoc. apply Qplus_le_r.
+    apply (Qle_trans _ ((2#p) + (1#p))).
+    apply Qplus_le_r.
+    unfold Qle, Qnum, Qden. do 2 rewrite Z.mul_1_l.
+    apply Pos2Z.pos_le_pos. apply Pos2Nat.inj_le.
+    rewrite Nat2Pos.id. apply le_S, le_refl. discriminate.
+    rewrite Qinv_plus_distr. unfold Qle, Qnum, Qden.
+    apply Z.mul_le_mono_nonneg_r. discriminate. discriminate.
+  - apply (Qle_trans _ (q + (r-q))). 2: ring_simplify; apply Qle_refl.
+    apply Qplus_le_r.
+    apply (Qmult_le_l _ _ ( (Z.pos p # 1) / (r-q))).
+    rewrite <- (Qmult_0_r (Z.pos p #1)). apply Qmult_lt_l.
+    reflexivity. apply Qinv_lt_0_compat.
+    unfold Qminus. rewrite <- Qlt_minus_iff. apply rmaj.
+    unfold Qdiv. rewrite Qmult_comm, <- Qmult_assoc.
+    rewrite (Qmult_comm (/(r-q))), Qmult_inv_r, Qmult_assoc.
+    setoid_replace ((4 # p) * (Z.pos p # 1))%Q with 4%Q.
+    2: reflexivity. rewrite Qmult_1_r.
+    apply Qlt_le_weak, pmaj. intro abs. destruct rmaj.
+    apply Qlt_minus_iff in H0.
+    rewrite abs in H0. apply (Qlt_not_le _ _ H0), Qle_refl.
+Qed.
+
+Lemma DRealReprQup : forall (x : DReal) (q : Q),
+    proj1_sig x q = false
+    -> CRealLe (DRealRepr x) (inject_Q q).
+Proof.
+  intros x q H [p pmaj].
+  unfold inject_Q, DRealRepr, proj1_sig in pmaj.
+  destruct (DRealQlim x (Pos.to_nat p)) as [r rmaj], rmaj.
+  clear H1. destruct x as [f low], low; unfold proj1_sig in H, H0.
+  apply (Qplus_lt_l _ _ q) in pmaj. ring_simplify in pmaj.
+  rewrite (e _ r) in H. discriminate. 2: exact H0.
+  apply Qlt_le_weak. apply (Qlt_trans _ ((2#p)+q)). 2: exact pmaj.
+  apply (Qplus_lt_l _ _ (-q)). ring_simplify. reflexivity.
+Qed.
+
+Lemma DRealQuot1 : forall x y:DReal, CRealEq (DRealRepr x) (DRealRepr y) -> x = y.
+Proof.
+  intros. destruct H. apply Rle_antisym.
+  - clear H. intros q H1. destruct (proj1_sig y q) eqn:des.
+    reflexivity. exfalso. apply H0.
+    apply (CReal_le_lt_trans _ (inject_Q q)). apply DRealReprQup.
+    exact des. apply DRealReprQ. exact H1.
+  - clear H0. intros q H1. destruct (proj1_sig x q) eqn:des.
+    reflexivity. exfalso. apply H.
+    apply (CReal_le_lt_trans _ (inject_Q q)). apply DRealReprQup.
+    exact des. apply DRealReprQ. exact H1.
+Qed.
+
+Lemma DRealAbstrFalse : forall (x : CReal) (q : Q) (n : nat),
+    proj1_sig (DRealAbstr x) q = false
+    -> (proj1_sig x (S n) <= q + (1 # Pos.of_nat (S n)))%Q.
+Proof.
+  intros. destruct x as [xn xcau].
+  unfold DRealAbstr, proj1_sig in H.
+  destruct (
+        sig_forall_dec (fun n : nat => (xn (S n) <= q + (1 # Pos.of_nat (S n)))%Q)
+          (fun n : nat =>
+           match Qlt_le_dec (q + (1 # Pos.of_nat (S n))) (xn (S n)) with
+           | left q0 => right (Qlt_not_le (q + (1 # Pos.of_nat (S n))) (xn (S n)) q0)
+           | right q0 => left q0
+           end)).
+  discriminate. apply q0.
+Qed.
+
+Lemma DRealQuot2 : forall x:CReal, CRealEq (DRealRepr (DRealAbstr x)) x.
+Proof.
+  split.
+  - intros [p pmaj]. unfold DRealRepr, proj1_sig in pmaj.
+    destruct x as [xn xcau].
+    destruct (DRealQlim (DRealAbstr (exist _ xn xcau)) (Pos.to_nat p))
+      as [q [_ qmaj]].
+    (* By pmaj, q + 1/p < x as real numbers.
+       But by qmaj x <= q + 1/(p+1), contradiction. *)
+    apply (DRealAbstrFalse _ _ (pred (Pos.to_nat p))) in qmaj.
+    unfold proj1_sig in qmaj.
+    rewrite Nat.succ_pred in qmaj.
+    apply (Qlt_not_le _ _ pmaj), (Qplus_le_l _ _ q).
+    ring_simplify. apply (Qle_trans _ _ _ qmaj).
+    rewrite <- Qplus_assoc. apply Qplus_le_r.
+    rewrite Pos2Nat.id. apply (Qle_trans _ ((1#p)+(1#p))).
+    apply Qplus_le_l. unfold Qle, Qnum, Qden.
+    do 2 rewrite Z.mul_1_l.
+    apply Pos2Z.pos_le_pos. apply Pos2Nat.inj_le.
+    rewrite Nat2Pos.id. apply le_S, le_refl. discriminate.
+    rewrite Qinv_plus_distr. apply Qle_refl.
+    intro abs. pose proof (Pos2Nat.is_pos p).
+    rewrite abs in H. inversion H.
+  - intros [p pmaj]. unfold DRealRepr, proj1_sig in pmaj.
+    destruct x as [xn xcau].
+    destruct (DRealQlim (DRealAbstr (exist _ xn xcau)) (Pos.to_nat p))
+      as [q [qmaj _]].
+    (* By pmaj, x < q - 1/p *)
+    unfold DRealAbstr, proj1_sig in qmaj.
+    destruct (
+           sig_forall_dec (fun n : nat => (xn (S n) <= q + (1 # Pos.of_nat (S n)))%Q)
+             (fun n : nat =>
+              match Qlt_le_dec (q + (1 # Pos.of_nat (S n))) (xn (S n)) with
+              | left q0 =>
+                  right (Qlt_not_le (q + (1 # Pos.of_nat (S n))) (xn (S n)) q0)
+              | right q0 => left q0
+              end)).
+    2: discriminate. clear qmaj.
+    destruct s as [n nmaj]. apply nmaj.
+    apply (Qplus_lt_l _ _ (xn (Pos.to_nat p) + (1#Pos.of_nat (S n)))) in pmaj.
+    ring_simplify in pmaj. apply Qlt_le_weak. rewrite Qplus_comm.
+    apply (Qlt_trans _ ((2 # p) + xn (Pos.to_nat p) + (1 # Pos.of_nat (S n)))).
+    2: exact pmaj.
+    apply (Qplus_lt_l _ _ (-xn (Pos.to_nat p))).
+    apply (Qle_lt_trans _ _ _ (Qle_Qabs _)).
+    destruct (le_lt_dec (S n) (Pos.to_nat p)).
+    + specialize (xcau (Pos.of_nat (S n)) (S n) (Pos.to_nat p)).
+      apply (Qlt_trans _ (1# Pos.of_nat (S n))). apply xcau.
+      rewrite Nat2Pos.id. apply le_refl. discriminate.
+      rewrite Nat2Pos.id. exact l. discriminate.
+      apply (Qplus_lt_l _ _ (-(1#Pos.of_nat (S n)))).
+      ring_simplify. reflexivity.
+    + apply (Qlt_trans _ (1#p)). apply xcau.
+      apply le_S_n in l. apply le_S, l. apply le_refl.
+      ring_simplify. apply (Qlt_trans _ (2#p)).
+      unfold Qlt, Qnum, Qden.
+      apply Z.mul_lt_mono_pos_r. reflexivity. reflexivity.
+      apply (Qplus_lt_l _ _ (-(2#p))). ring_simplify. reflexivity.
+Qed.
diff --git a/theories/Reals/ConstructiveCauchyReals.v b/theories/Reals/ConstructiveCauchyReals.v
index 965d31d403..b83f8581d0 100644
--- a/theories/Reals/ConstructiveCauchyReals.v
+++ b/theories/Reals/ConstructiveCauchyReals.v
@@ -16,15 +16,7 @@ Require Import Logic.ConstructiveEpsilon.
 Require CMorphisms.
 
 (** The constructive Cauchy real numbers, ie the Cauchy sequences
-    of rational numbers. This file is not supposed to be imported,
-    except in Rdefinitions.v, Raxioms.v, Rcomplete_constr.v
-    and ConstructiveRIneq.v.
-
-    Constructive real numbers should be considered abstractly,
-    forgetting the fact that they are implemented as rational sequences.
-    All useful lemmas of this file are exposed in ConstructiveRIneq.v,
-    under more abstract names, like Rlt_asym instead of CRealLt_asym.
-
+    of rational numbers.
 
     Cauchy reals are Cauchy sequences of rational numbers,
     equipped with explicit moduli of convergence and
@@ -705,6 +697,17 @@ Proof.
     right. rewrite H0, H. exact c.
 Qed.
 
+Add Parametric Morphism : CRealLtProp
+    with signature CRealEq ==> CRealEq ==> iff
+      as CRealLtProp_morph.
+Proof.
+  intros x y H x0 y0 H0. split.
+  - intro. apply CRealLtForget. apply CRealLtEpsilon in H1.
+    rewrite <- H, <- H0. exact H1.
+  - intro. apply CRealLtForget. apply CRealLtEpsilon in H1.
+    rewrite H, H0. exact H1.
+Qed.
+
 Add Parametric Morphism : CRealLe
     with signature CRealEq ==> CRealEq ==> iff
       as CRealLe_morph.
@@ -772,6 +775,9 @@ Proof.
   intro q. exists (fun n => q). apply ConstCauchy.
 Defined.
 
+Definition inject_Z : Z -> CReal
+  := fun n => inject_Q (n # 1).
+
 Notation "0" := (inject_Q 0) : CReal_scope.
 Notation "1" := (inject_Q 1) : CReal_scope.
 Notation "2" := (inject_Q 2) : CReal_scope.
@@ -1324,3 +1330,19 @@ Proof.
   apply (Qlt_not_le _ _ maj). apply (Qle_trans _ 0).
   apply (Qplus_le_l _ _ r). ring_simplify. exact H. discriminate.
 Qed.
+
+Lemma inject_Z_plus : forall q r : Z,
+    inject_Z (q + r) == inject_Z q + inject_Z r.
+Proof.
+  intros. unfold inject_Z.
+  setoid_replace (q + r # 1)%Q with ((q#1) + (r#1))%Q.
+  apply inject_Q_plus. rewrite Qinv_plus_distr. reflexivity.
+Qed.
+
+Lemma opp_inject_Z : forall n : Z,
+    inject_Z (-n) == - inject_Z n.
+Proof.
+  intros. unfold inject_Z.
+  setoid_replace (-n # 1)%Q with (-(n#1))%Q.
+  rewrite opp_inject_Q. reflexivity. reflexivity.
+Qed.
diff --git a/theories/Reals/ConstructiveRIneq.v b/theories/Reals/ConstructiveRIneq.v
deleted file mode 100644
index e0f08d2fbe..0000000000
--- a/theories/Reals/ConstructiveRIneq.v
+++ /dev/null
@@ -1,2817 +0,0 @@
-(************************************************************************)
-(*         *   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)         *)
-(************************************************************************)
-(************************************************************************)
-
-(*********************************************************)
-(** * Basic lemmas for the contructive real numbers      *)
-(*********************************************************)
-
-(* Implement interface ConstructiveReals opaquely with
-   Cauchy reals and prove basic results.
-   Those are therefore true for any implementation of
-   ConstructiveReals (for example with Dedekind reals).
-
-   This file is the recommended import for working with
-   constructive reals, do not use ConstructiveCauchyReals
-   directly. *)
-
-Require Import ConstructiveCauchyRealsMult.
-Require Import ConstructiveRcomplete.
-Require Export ConstructiveReals.
-Require Import Zpower.
-Require Export ZArithRing.
-Require Import Omega.
-Require Import QArith_base.
-Require Import Qring.
-
-Declare Scope R_scope_constr.
-
-Local Open Scope Z_scope.
-Local Open Scope R_scope_constr.
-
-Definition CRealImplem : ConstructiveReals.
-Proof.
-  assert (isLinearOrder CReal CRealLt) as lin.
-  { repeat split. exact CRealLt_asym.
-    exact CReal_lt_trans.
-    intros. destruct (CRealLt_dec x z y H).
-    left. exact c. right. exact c. }
-  apply (Build_ConstructiveReals
-           CReal CRealLt lin CRealLtProp
-           CRealLtEpsilon CRealLtForget CRealLtDisjunctEpsilon
-           (inject_Q 0) (inject_Q 1)
-           CReal_plus CReal_opp CReal_mult
-           CReal_isRing CReal_isRingExt CRealLt_0_1
-           CReal_plus_lt_compat_l CReal_plus_lt_reg_l
-           CReal_mult_lt_0_compat
-           CReal_inv CReal_inv_l CReal_inv_0_lt_compat
-           inject_Q inject_Q_plus inject_Q_mult
-           inject_Q_one inject_Q_lt lt_inject_Q
-           CRealQ_dense Rup_pos).
-  - intros. destruct (Rcauchy_complete xn) as [l cv].
-    intro n. destruct (H n). exists x. intros.
-    specialize (a i j H0 H1) as [a b]. split. 2: exact b.
-    rewrite <- opp_inject_Q.
-    setoid_replace (-(1#n))%Q with (-1#n). exact a. reflexivity.
-    exists l. intros p. destruct (cv p).
-    exists x. intros. specialize (a i H0). split. 2: apply a.
-    unfold orderLe.
-    intro abs. setoid_replace (-1#p) with (-(1#p))%Q in abs.
-    rewrite opp_inject_Q in abs. destruct a. contradiction.
-    reflexivity.
-Defined.
-
-Definition CR : ConstructiveReals.
-Proof.
-  exact CRealImplem.
-Qed. (* Keep it opaque to possibly change the implementation later *)
-
-Definition R := CRcarrier CR.
-
-Definition Req := orderEq R (CRlt CR).
-Definition Rle (x y : R) := CRlt CR y x -> False.
-Definition Rge (x y : R) := CRlt CR x y -> False.
-Definition Rlt := CRlt CR.
-Definition RltProp := CRltProp CR.
-Definition Rgt (x y : R) := CRlt CR y x.
-Definition Rappart := orderAppart R (CRlt CR).
-
-Infix "==" := Req : R_scope_constr.
-Infix "#" := Rappart : R_scope_constr.
-Infix "<" := Rlt : R_scope_constr.
-Infix ">" := Rgt : R_scope_constr.
-Infix "<=" := Rle : R_scope_constr.
-Infix ">=" := Rge : R_scope_constr.
-
-Notation "x <= y <= z" := (x <= y /\ y <= z) : R_scope_constr.
-Notation "x <= y < z"  := (prod (x <= y) (y < z)) : R_scope_constr.
-Notation "x < y < z"   := (prod (x < y) (y < z)) : R_scope_constr.
-Notation "x < y <= z"  := (prod (x < y) (y <= z)) : R_scope_constr.
-
-Lemma Rlt_epsilon : forall x y : R, RltProp x y -> x < y.
-Proof.
-  exact (CRltEpsilon CR).
-Qed.
-
-Lemma Rlt_forget : forall x y : R, x < y -> RltProp x y.
-Proof.
-  exact (CRltForget CR).
-Qed.
-
-Lemma Rle_refl : forall x : R, x <= x.
-Proof.
-  intros. intro abs.
-  destruct (CRltLinear CR), p.
-  exact (f x x abs abs).
-Qed.
-Hint Immediate Rle_refl: rorders.
-
-Lemma Req_refl : forall x : R, x == x.
-Proof.
-  intros. split; apply Rle_refl.
-Qed.
-
-Lemma Req_sym : forall x y : R, x == y -> y == x.
-Proof.
-  intros. destruct H. split; intro abs; contradiction.
-Qed.
-
-Lemma Req_trans : forall x y z : R, x == y -> y == z -> x == z.
-Proof.
-  intros. destruct H,H0. destruct (CRltLinear CR), p. split.
-  - intro abs. destruct (s _ y _ abs); contradiction.
-  - intro abs. destruct (s _ y _ abs); contradiction.
-Qed.
-
-Add Parametric Relation : R Req
-    reflexivity proved by Req_refl
-    symmetry proved by Req_sym
-    transitivity proved by Req_trans
-      as Req_rel.
-
-Instance Req_relT : CRelationClasses.Equivalence Req.
-Proof.
-  split. exact Req_refl. exact Req_sym. exact Req_trans.
-Qed.
-
-Lemma linear_order_T : forall x y z : R,
-    x < z -> (x < y) + (y < z).
-Proof.
-  intros. destruct (CRltLinear CR). apply s. exact H.
-Qed.
-
-Instance Rlt_morph
-  : CMorphisms.Proper
-      (CMorphisms.respectful Req (CMorphisms.respectful Req CRelationClasses.iffT)) Rlt.
-Proof.
-  intros x y H x0 y0 H0. destruct H, H0. split.
-  - intro. destruct (linear_order_T x y x0). assumption.
-    contradiction. destruct (linear_order_T y y0 x0).
-    assumption. assumption. contradiction.
-  - intro. destruct (linear_order_T y x y0). assumption.
-    contradiction. destruct (linear_order_T x x0 y0).
-    assumption. assumption. contradiction.
-Qed.
-
-Instance RltProp_morph
-  : Morphisms.Proper
-      (Morphisms.respectful Req (Morphisms.respectful Req iff)) RltProp.
-Proof.
-  intros x y H x0 y0 H0. destruct H, H0. split.
-  - intro. destruct (linear_order_T x y x0).
-    apply Rlt_epsilon. assumption.
-    contradiction. destruct (linear_order_T y y0 x0).
-    assumption. apply Rlt_forget. assumption. contradiction.
-  - intro. destruct (linear_order_T y x y0).
-    apply Rlt_epsilon. assumption.
-    contradiction. destruct (linear_order_T x x0 y0).
-    assumption. apply Rlt_forget. assumption. contradiction.
-Qed.
-
-Instance Rgt_morph
-  : CMorphisms.Proper
-      (CMorphisms.respectful Req (CMorphisms.respectful Req CRelationClasses.iffT)) Rgt.
-Proof.
-  intros x y H x0 y0 H0. unfold Rgt. apply Rlt_morph; assumption.
-Qed.
-
-Instance Rappart_morph
-  : CMorphisms.Proper
-      (CMorphisms.respectful Req (CMorphisms.respectful Req CRelationClasses.iffT)) Rappart.
-Proof.
-  split.
-  - intros. destruct H1. left. rewrite <- H0, <- H. exact c.
-    right. rewrite <- H0, <- H. exact c.
-  - intros. destruct H1. left. rewrite H0, H. exact c.
-    right. rewrite H0, H. exact c.
-Qed.
-
-Add Parametric Morphism : Rle
-    with signature Req ==> Req ==> iff
-      as Rle_morph.
-Proof.
-  intros. split.
-  - intros H1 H2. unfold CRealLe in H1.
-    rewrite <- H0 in H2. rewrite <- H in H2. contradiction.
-  - intros H1 H2. unfold CRealLe in H1.
-    rewrite H0 in H2. rewrite H in H2. contradiction.
-Qed.
-
-Add Parametric Morphism : Rge
-    with signature Req ==> Req ==> iff
-      as Rge_morph.
-Proof.
-  intros. unfold Rge. apply Rle_morph; assumption.
-Qed.
-
-
-Definition Rplus := CRplus CR.
-Definition Rmult := CRmult CR.
-Definition Rinv := CRinv CR.
-Definition Ropp := CRopp CR.
-
-Add Parametric Morphism : Rplus
-    with signature Req ==> Req ==> Req
-      as Rplus_morph.
-Proof.
-  apply CRisRingExt.
-Qed.
-
-Instance Rplus_morph_T
-  : CMorphisms.Proper
-      (CMorphisms.respectful Req (CMorphisms.respectful Req Req)) Rplus.
-Proof.
-  apply CRisRingExt.
-Qed.
-
-Add Parametric Morphism : Rmult
-    with signature Req ==> Req ==> Req
-      as Rmult_morph.
-Proof.
-  apply CRisRingExt.
-Qed.
-
-Instance Rmult_morph_T
-  : CMorphisms.Proper
-      (CMorphisms.respectful Req (CMorphisms.respectful Req Req)) Rmult.
-Proof.
-  apply CRisRingExt.
-Qed.
-
-Add Parametric Morphism : Ropp
-    with signature Req ==> Req
-      as Ropp_morph.
-Proof.
-  apply CRisRingExt.
-Qed.
-
-Instance Ropp_morph_T
-  : CMorphisms.Proper
-      (CMorphisms.respectful Req Req) Ropp.
-Proof.
-  apply CRisRingExt.
-Qed.
-
-Infix "+" := Rplus : R_scope_constr.
-Notation "- x" := (Ropp x) : R_scope_constr.
-Definition Rminus (r1 r2:R) : R := r1 + - r2.
-Infix "-" := Rminus : R_scope_constr.
-Infix "*" := Rmult : R_scope_constr.
-Notation "/ x" := (CRinv CR x) (at level 35, right associativity) : R_scope_constr.
-
-Notation "0" := (CRzero CR) : R_scope_constr.
-Notation "1" := (CRone CR) : R_scope_constr.
-
-Add Parametric Morphism : Rminus
-    with signature Req ==> Req ==> Req
-      as Rminus_morph.
-Proof.
-  intros. unfold Rminus, CRminus. rewrite H,H0. reflexivity.
-Qed.
-
-
-(* Help Add Ring to find the correct equality *)
-Lemma RisRing : ring_theory 0 1
-                            Rplus Rmult
-                            Rminus Ropp
-                            Req.
-Proof.
-  exact (CRisRing CR).
-Qed.
-
-Add Ring CRealRing : RisRing.
-
-Lemma Rplus_comm : forall x y:R, x + y == y + x.
-Proof. intros. ring. Qed.
-
-Lemma Rplus_assoc : forall x y z:R, (x + y) + z == x + (y + z).
-Proof. intros. ring. Qed.
-
-Lemma Rplus_opp_r : forall x:R, x + -x == 0.
-Proof. intros. ring. Qed.
-
-Lemma Rplus_0_l : forall x:R, 0 + x == x.
-Proof. intros. ring. Qed.
-
-Lemma Rmult_0_l : forall x:R, 0 * x == 0.
-Proof. intros. ring. Qed.
-
-Lemma Rmult_1_l : forall x:R, 1 * x == x.
-Proof. intros. ring. Qed.
-
-Lemma Rmult_comm : forall x y:R, x * y == y * x.
-Proof. intros. ring. Qed.
-
-Lemma Rmult_assoc : forall x y z:R, (x * y) * z == x * (y * z).
-Proof. intros. ring. Qed.
-
-Definition Rinv_l := CRinv_l CR.
-
-Lemma Rmult_plus_distr_l : forall r1 r2 r3 : R,
-    r1 * (r2 + r3) == (r1 * r2) + (r1 * r3).
-Proof. intros. ring. Qed.
-
-Definition Rlt_0_1 := CRzero_lt_one CR.
-
-Lemma Rlt_asym : forall x y :R, x < y -> y < x -> False.
-Proof.
-  intros. destruct (CRltLinear CR), p.
-  apply (f x y); assumption.
-Qed.
-
-Lemma Rlt_trans : forall x y z : R, x < y -> y < z -> x < z.
-Proof.
-  intros. destruct (CRltLinear CR), p.
-  apply (c x y); assumption.
-Qed.
-
-Lemma Rplus_lt_compat_l : forall x y z : R,
-    y < z -> x + y < x + z.
-Proof.
-  intros. apply CRplus_lt_compat_l. exact H.
-Qed.
-
-Lemma Ropp_mult_distr_l
-  : forall r1 r2 : R, -(r1 * r2) == (- r1) * r2.
-Proof.
-  intros. ring.
-Qed.
-
-Lemma Rplus_lt_reg_l : forall r r1 r2, r + r1 < r + r2 -> r1 < r2.
-Proof.
-  intros. apply CRplus_lt_reg_l in H. exact H.
-Qed.
-
-Lemma Rmult_lt_compat_l : forall x y z : R,
-    0 < x -> y < z -> x * y < x * z.
-Proof.
-  intros. apply (CRplus_lt_reg_l CR (- (x * y))).
-  rewrite Rplus_comm. pose proof Rplus_opp_r.
-  rewrite H1.
-  rewrite Rmult_comm, Ropp_mult_distr_l, Rmult_comm.
-  rewrite <- Rmult_plus_distr_l.
-  apply CRmult_lt_0_compat. exact H.
-  apply (Rplus_lt_reg_l y).
-  rewrite Rplus_comm, Rplus_0_l.
-  rewrite <- Rplus_assoc, H1, Rplus_0_l. exact H0.
-Qed.
-
-Hint Resolve Rplus_comm Rplus_assoc Rplus_opp_r Rplus_0_l
-     Rmult_comm Rmult_assoc Rinv_l Rmult_1_l Rmult_plus_distr_l
-     Rlt_0_1 Rlt_asym Rlt_trans Rplus_lt_compat_l Rmult_lt_compat_l
-     Rmult_0_l : creal.
-
-Fixpoint INR (n:nat) : R :=
-  match n with
-  | O => 0
-  | S O => 1
-  | S n => INR n + 1
-  end.
-Arguments INR n%nat.
-
-(* compact representation for 2*p *)
-Fixpoint IPR_2 (p:positive) : R :=
-  match p with
-  | xH => 1 + 1
-  | xO p => (1 + 1) * IPR_2 p
-  | xI p => (1 + 1) * (1 + IPR_2 p)
-  end.
-
-Definition IPR (p:positive) : R :=
-  match p with
-  | xH => 1
-  | xO p => IPR_2 p
-  | xI p => 1 + IPR_2 p
-  end.
-Arguments IPR p%positive : simpl never.
-
-(**********)
-Definition IZR (z:Z) : R :=
-  match z with
-  | Z0 => 0
-  | Zpos n => IPR n
-  | Zneg n => - IPR n
-  end.
-Arguments IZR z%Z : simpl never.
-
-Notation "2" := (IZR 2) : R_scope_constr.
-
-
-(*********************************************************)
-(** ** Relation between orders and equality              *)
-(*********************************************************)
-
-Lemma Rge_refl : forall r, r <= r.
-Proof. exact Rle_refl. Qed.
-Hint Immediate Rge_refl: rorders.
-
-(** Irreflexivity of the strict order *)
-
-Lemma Rlt_irrefl : forall r, r < r -> False.
-Proof.
-  intros r H; eapply Rlt_asym; eauto.
-Qed.
-Hint Resolve Rlt_irrefl: creal.
-
-Lemma Rgt_irrefl : forall r, r > r -> False.
-Proof. exact Rlt_irrefl. Qed.
-
-Lemma Rlt_not_eq : forall r1 r2, r1 < r2 -> r1 <> r2.
-Proof.
-  intros. intro abs. subst r2. exact (Rlt_irrefl r1 H).
-Qed.
-
-Lemma Rgt_not_eq : forall r1 r2, r1 > r2 -> r1 <> r2.
-Proof.
-  intros; apply not_eq_sym; apply Rlt_not_eq; auto with creal.
-Qed.
-
-(**********)
-Lemma Rlt_dichotomy_converse : forall r1 r2, ((r1 < r2) + (r1 > r2)) -> r1 <> r2.
-Proof.
-  intros. destruct H.
-  - intro abs. subst r2. exact (Rlt_irrefl r1 r).
-  - intro abs. subst r2. exact (Rlt_irrefl r1 r).
-Qed.
-Hint Resolve Rlt_dichotomy_converse: creal.
-
-(** Reasoning by case on equality and order *)
-
-
-(*********************************************************)
-(** ** Relating [<], [>], [<=] and [>=]  	         *)
-(*********************************************************)
-
-(*********************************************************)
-(** ** Order                                             *)
-(*********************************************************)
-
-(** *** Relating strict and large orders *)
-
-Lemma Rlt_le : forall r1 r2, r1 < r2 -> r1 <= r2.
-Proof.
-  intros. intro abs. apply (Rlt_asym r1 r2); assumption.
-Qed.
-Hint Resolve Rlt_le: creal.
-
-Lemma Rgt_ge : forall r1 r2, r1 > r2 -> r1 >= r2.
-Proof.
-  intros. intro abs. apply (Rlt_asym r1 r2); assumption.
-Qed.
-
-(**********)
-Lemma Rle_ge : forall r1 r2, r1 <= r2 -> r2 >= r1.
-Proof.
-  intros. intros abs. contradiction.
-Qed.
-Hint Immediate Rle_ge: creal.
-Hint Resolve Rle_ge: rorders.
-
-Lemma Rge_le : forall r1 r2, r1 >= r2 -> r2 <= r1.
-Proof.
-  intros. intro abs. contradiction.
-Qed.
-Hint Resolve Rge_le: creal.
-Hint Immediate Rge_le: rorders.
-
-(**********)
-Lemma Rlt_gt : forall r1 r2, r1 < r2 -> r2 > r1.
-Proof.
-  trivial.
-Qed.
-Hint Resolve Rlt_gt: rorders.
-
-Lemma Rgt_lt : forall r1 r2, r1 > r2 -> r2 < r1.
-Proof.
-  trivial.
-Qed.
-Hint Immediate Rgt_lt: rorders.
-
-(**********)
-
-Lemma Rnot_lt_le : forall r1 r2, (r1 < r2 -> False) -> r2 <= r1.
-Proof.
-  intros. exact H.
-Qed.
-
-Lemma Rnot_gt_le : forall r1 r2, (r1 > r2 -> False) -> r1 <= r2.
-Proof.
-  intros. intro abs. contradiction.
-Qed.
-
-Lemma Rnot_gt_ge : forall r1 r2, (r1 > r2 -> False) -> r2 >= r1.
-Proof.
-  intros. intro abs. contradiction.
-Qed.
-
-Lemma Rnot_lt_ge : forall r1 r2, (r1 < r2 -> False) -> r1 >= r2.
-Proof.
-  intros. intro abs. contradiction.
-Qed.
-
-(**********)
-Lemma Rlt_not_le : forall r1 r2, r2 < r1 -> ~ r1 <= r2.
-Proof.
-  generalize Rlt_asym Rlt_dichotomy_converse; unfold CRealLe.
-  unfold not; intuition eauto 3.
-Qed.
-Hint Immediate Rlt_not_le: creal.
-
-Lemma Rgt_not_le : forall r1 r2, r1 > r2 -> ~ r1 <= r2.
-Proof. exact Rlt_not_le. Qed.
-
-Lemma Rlt_not_ge : forall r1 r2, r1 < r2 -> ~ r1 >= r2.
-Proof. red; intros; eapply Rlt_not_le; eauto with creal. Qed.
-Hint Immediate Rlt_not_ge: creal.
-
-Lemma Rgt_not_ge : forall r1 r2, r2 > r1 -> ~ r1 >= r2.
-Proof. exact Rlt_not_ge. Qed.
-
-Lemma Rle_not_lt : forall r1 r2, r2 <= r1 -> r1 < r2 -> False.
-Proof.
-  intros r1 r2. generalize (Rlt_asym r1 r2) (Rlt_dichotomy_converse r1 r2).
-  unfold CRealLe; intuition.
-Qed.
-
-Lemma Rge_not_lt : forall r1 r2, r1 >= r2 -> r1 < r2 -> False.
-Proof. intros; apply (Rle_not_lt r1 r2); auto with creal. Qed.
-
-Lemma Rle_not_gt : forall r1 r2, r1 <= r2 -> r1 > r2 -> False.
-Proof. do 2 intro; apply Rle_not_lt. Qed.
-
-Lemma Rge_not_gt : forall r1 r2, r2 >= r1 -> r1 > r2 -> False.
-Proof. do 2 intro; apply Rge_not_lt. Qed.
-
-(**********)
-Lemma Req_le : forall r1 r2, r1 = r2 -> r1 <= r2.
-Proof.
-  intros. intro abs. subst r2. exact (Rlt_irrefl r1 abs).
-Qed.
-Hint Immediate Req_le: creal.
-
-Lemma Req_ge : forall r1 r2, r1 = r2 -> r1 >= r2.
-Proof.
-  intros. intro abs. subst r2. exact (Rlt_irrefl r1 abs).
-Qed.
-Hint Immediate Req_ge: creal.
-
-Lemma Req_le_sym : forall r1 r2, r2 = r1 -> r1 <= r2.
-Proof.
-  intros. intro abs. subst r2. exact (Rlt_irrefl r1 abs).
-Qed.
-Hint Immediate Req_le_sym: creal.
-
-Lemma Req_ge_sym : forall r1 r2, r2 = r1 -> r1 >= r2.
-Proof.
-  intros. intro abs. subst r2. exact (Rlt_irrefl r1 abs).
-Qed.
-Hint Immediate Req_ge_sym: creal.
-
-(** *** Asymmetry *)
-
-(** Remark: [Rlt_asym] is an axiom *)
-
-Lemma Rgt_asym : forall r1 r2, r1 > r2 -> r2 > r1 -> False.
-Proof. do 2 intro; apply Rlt_asym. Qed.
-
-
-(** *** Compatibility with equality *)
-
-Lemma Rlt_eq_compat :
-  forall r1 r2 r3 r4, r1 = r2 -> r2 < r4 -> r4 = r3 -> r1 < r3.
-Proof.
-  intros x x' y y'; intros; replace x with x'; replace y with y'; assumption.
-Qed.
-
-Lemma Rgt_eq_compat :
-  forall r1 r2 r3 r4, r1 = r2 -> r2 > r4 -> r4 = r3 -> r1 > r3.
-Proof. intros; red; apply Rlt_eq_compat with (r2:=r4) (r4:=r2); auto. Qed.
-
-(** *** Transitivity *)
-
-Lemma Rle_trans : forall r1 r2 r3, r1 <= r2 -> r2 <= r3 -> r1 <= r3.
-Proof.
-  intros. intro abs.
-  destruct (linear_order_T r3 r2 r1 abs); contradiction.
-Qed.
-
-Lemma Rge_trans : forall r1 r2 r3, r1 >= r2 -> r2 >= r3 -> r1 >= r3.
-Proof.
-  intros. apply (Rle_trans _ r2); assumption.
-Qed.
-
-Lemma Rgt_trans : forall r1 r2 r3, r1 > r2 -> r2 > r3 -> r1 > r3.
-Proof.
-  intros. apply (Rlt_trans _ r2); assumption.
-Qed.
-
-(**********)
-Lemma Rle_lt_trans : forall r1 r2 r3, r1 <= r2 -> r2 < r3 -> r1 < r3.
-Proof.
-  intros.
-  destruct (linear_order_T r2 r1 r3 H0). contradiction. apply r.
-Qed.
-
-Lemma Rlt_le_trans : forall r1 r2 r3, r1 < r2 -> r2 <= r3 -> r1 < r3.
-Proof.
-  intros.
-  destruct (linear_order_T r1 r3 r2 H). apply r. contradiction.
-Qed.
-
-Lemma Rge_gt_trans : forall r1 r2 r3, r1 >= r2 -> r2 > r3 -> r1 > r3.
-Proof.
-  intros. apply (Rlt_le_trans _ r2); assumption.
-Qed.
-
-Lemma Rgt_ge_trans : forall r1 r2 r3, r1 > r2 -> r2 >= r3 -> r1 > r3.
-Proof.
-  intros. apply (Rle_lt_trans _ r2); assumption.
-Qed.
-
-
-(*********************************************************)
-(** ** Addition                                          *)
-(*********************************************************)
-
-(** Remark: [Rplus_0_l] is an axiom *)
-
-Lemma Rplus_0_r : forall r, r + 0 == r.
-Proof.
-  intros. rewrite Rplus_comm. rewrite Rplus_0_l. reflexivity.
-Qed.
-Hint Resolve Rplus_0_r: creal.
-
-Lemma Rplus_ne : forall r, r + 0 == r /\ 0 + r == r.
-Proof.
-  split. apply Rplus_0_r. apply Rplus_0_l.
-Qed.
-Hint Resolve Rplus_ne: creal.
-
-(**********)
-
-(** Remark: [Rplus_opp_r] is an axiom *)
-
-Lemma Rplus_opp_l : forall r, - r + r == 0.
-Proof.
-  intros. rewrite Rplus_comm. apply Rplus_opp_r.
-Qed.
-Hint Resolve Rplus_opp_l: creal.
-
-(**********)
-Lemma Rplus_opp_r_uniq : forall r1 r2, r1 + r2 == 0 -> r2 == - r1.
-Proof.
-  intros x y H. rewrite <- (Rplus_0_l y).
-  rewrite <- (Rplus_opp_l x). rewrite Rplus_assoc.
-  rewrite H. rewrite Rplus_0_r. reflexivity.
-Qed.
-
-Lemma Rplus_eq_compat_l : forall r r1 r2, r1 == r2 -> r + r1 == r + r2.
-Proof.
-  intros. rewrite H. reflexivity.
-Qed.
-
-Lemma Rplus_eq_compat_r : forall r r1 r2, r1 == r2 -> r1 + r == r2 + r.
-Proof.
-  intros. rewrite H. reflexivity.
-Qed.
-
-
-(**********)
-Lemma Rplus_eq_reg_l : forall r r1 r2, r + r1 == r + r2 -> r1 == r2.
-Proof.
-  intros; transitivity (- r + r + r1).
-  rewrite Rplus_opp_l. rewrite Rplus_0_l. reflexivity.
-  transitivity (- r + r + r2).
-  repeat rewrite Rplus_assoc; rewrite <- H; reflexivity.
-  rewrite Rplus_opp_l. rewrite Rplus_0_l. reflexivity.
-Qed.
-Hint Resolve Rplus_eq_reg_l: creal.
-
-Lemma Rplus_eq_reg_r : forall r r1 r2, r1 + r == r2 + r -> r1 == r2.
-Proof.
-  intros r r1 r2 H.
-  apply Rplus_eq_reg_l with r.
-  now rewrite 2!(Rplus_comm r).
-Qed.
-
-(**********)
-Lemma Rplus_0_r_uniq : forall r r1, r + r1 == r -> r1 == 0.
-Proof.
-  intros. apply (Rplus_eq_reg_l r). rewrite Rplus_0_r. exact H.
-Qed.
-
-
-(*********************************************************)
-(** ** Multiplication                                    *)
-(*********************************************************)
-
-(**********)
-Lemma Rinv_r : forall r (rnz : r # 0),
-    r # 0 -> r * ((/ r) rnz) == 1.
-Proof.
-  intros. rewrite Rmult_comm. rewrite Rinv_l.
-  reflexivity.
-Qed.
-Hint Resolve Rinv_r: creal.
-
-Lemma Rinv_l_sym : forall r (rnz: r # 0), 1 == (/ r) rnz * r.
-Proof.
-  intros. symmetry. apply Rinv_l.
-Qed.
-Hint Resolve Rinv_l_sym: creal.
-
-Lemma Rinv_r_sym : forall r (rnz : r # 0), 1 == r * (/ r) rnz.
-Proof.
-  intros. symmetry. apply Rinv_r. apply rnz.
-Qed.
-Hint Resolve Rinv_r_sym: creal.
-
-(**********)
-Lemma Rmult_0_r : forall r, r * 0 == 0.
-Proof.
-  intro; ring.
-Qed.
-Hint Resolve Rmult_0_r: creal.
-
-(**********)
-Lemma Rmult_ne : forall r, r * 1 == r /\ 1 * r == r.
-Proof.
-  intro; split; ring.
-Qed.
-Hint Resolve Rmult_ne: creal.
-
-(**********)
-Lemma Rmult_1_r : forall r, r * 1 == r.
-Proof.
-  intro; ring.
-Qed.
-Hint Resolve Rmult_1_r: creal.
-
-(**********)
-Lemma Rmult_eq_compat_l : forall r r1 r2, r1 == r2 -> r * r1 == r * r2.
-Proof.
-  intros. rewrite H. reflexivity.
-Qed.
-
-Lemma Rmult_eq_compat_r : forall r r1 r2, r1 == r2 -> r1 * r == r2 * r.
-Proof.
-  intros. rewrite H. reflexivity.
-Qed.
-
-(**********)
-Lemma Rmult_eq_reg_l : forall r r1 r2, r * r1 == r * r2 -> r # 0 -> r1 == r2.
-Proof.
-  intros. transitivity ((/ r) H0 * r * r1).
-  rewrite Rinv_l. ring.
-  transitivity ((/ r) H0 * r * r2).
-  repeat rewrite Rmult_assoc; rewrite H; reflexivity.
-  rewrite Rinv_l. ring.
-Qed.
-
-Lemma Rmult_eq_reg_r : forall r r1 r2, r1 * r == r2 * r -> r # 0 -> r1 == r2.
-Proof.
-  intros.
-  apply Rmult_eq_reg_l with (2 := H0).
-  now rewrite 2!(Rmult_comm r).
-Qed.
-
-(**********)
-Lemma Rmult_eq_0_compat : forall r1 r2, r1 == 0 \/ r2 == 0 -> r1 * r2 == 0.
-Proof.
-  intros r1 r2 [H| H]; rewrite H; auto with creal.
-Qed.
-
-Hint Resolve Rmult_eq_0_compat: creal.
-
-(**********)
-Lemma Rmult_eq_0_compat_r : forall r1 r2, r1 == 0 -> r1 * r2 == 0.
-Proof.
-  auto with creal.
-Qed.
-
-(**********)
-Lemma Rmult_eq_0_compat_l : forall r1 r2, r2 == 0 -> r1 * r2 == 0.
-Proof.
-  auto with creal.
-Qed.
-
-(**********)
-Lemma Rmult_integral_contrapositive :
-  forall r1 r2, (prod (r1 # 0) (r2 # 0)) -> (r1 * r2) # 0.
-Proof.
-  assert (forall r, 0 > r -> 0 < - r).
-  { intros. rewrite <- (Rplus_opp_l r), <- (Rplus_0_r (-r)), Rplus_assoc.
-    apply Rplus_lt_compat_l. rewrite Rplus_0_l. apply H. }
-  intros. destruct H0, r, r0.
-  - right. setoid_replace (r1*r2) with (-r1 * -r2). 2: ring.
-    rewrite <- (Rmult_0_r (-r1)). apply Rmult_lt_compat_l; apply H; assumption.
-  - left. rewrite <- (Rmult_0_r r2).
-    rewrite Rmult_comm. apply (Rmult_lt_compat_l). apply c0. apply c.
-  - left. rewrite <- (Rmult_0_r r1). apply (Rmult_lt_compat_l). apply c. apply c0.
-  - right. rewrite <- (Rmult_0_r r1). apply Rmult_lt_compat_l; assumption.
-Qed.
-Hint Resolve Rmult_integral_contrapositive: creal.
-
-Lemma Rmult_integral_contrapositive_currified :
-  forall r1 r2, r1 # 0 -> r2 # 0 -> (r1 * r2) # 0.
-Proof.
-  intros. apply Rmult_integral_contrapositive.
-  split; assumption.
-Qed.
-
-(**********)
-Lemma Rmult_plus_distr_r :
-  forall r1 r2 r3, (r1 + r2) * r3 == r1 * r3 + r2 * r3.
-Proof.
-  intros; ring.
-Qed.
-
-(*********************************************************)
-(** ** Square function                                   *)
-(*********************************************************)
-
-(***********)
-Definition Rsqr (r : R) := r * r.
-
-Notation "r ²" := (Rsqr r) (at level 1, format "r ²") : R_scope_constr.
-
-(***********)
-Lemma Rsqr_0 : Rsqr 0 == 0.
-  unfold Rsqr; auto with creal.
-Qed.
-
-(*********************************************************)
-(** ** Opposite                                          *)
-(*********************************************************)
-
-(**********)
-Lemma Ropp_eq_compat : forall r1 r2, r1 == r2 -> - r1 == - r2.
-Proof.
-  intros. rewrite H. reflexivity.
-Qed.
-Hint Resolve Ropp_eq_compat: creal.
-
-(**********)
-Lemma Ropp_0 : -0 == 0.
-Proof.
-  ring.
-Qed.
-Hint Resolve Ropp_0: creal.
-
-(**********)
-Lemma Ropp_eq_0_compat : forall r, r == 0 -> - r == 0.
-Proof.
-  intros; rewrite H; auto with creal.
-Qed.
-Hint Resolve Ropp_eq_0_compat: creal.
-
-(**********)
-Lemma Ropp_involutive : forall r, - - r == r.
-Proof.
-  intro; ring.
-Qed.
-Hint Resolve Ropp_involutive: creal.
-
-(**********)
-Lemma Ropp_plus_distr : forall r1 r2, - (r1 + r2) == - r1 + - r2.
-Proof.
-  intros; ring.
-Qed.
-Hint Resolve Ropp_plus_distr: creal.
-
-(*********************************************************)
-(** ** Opposite and multiplication                       *)
-(*********************************************************)
-
-Lemma Ropp_mult_distr_l_reverse : forall r1 r2, - r1 * r2 == - (r1 * r2).
-Proof.
-  intros; ring.
-Qed.
-Hint Resolve Ropp_mult_distr_l_reverse: creal.
-
-(**********)
-Lemma Rmult_opp_opp : forall r1 r2, - r1 * - r2 == r1 * r2.
-Proof.
-  intros; ring.
-Qed.
-Hint Resolve Rmult_opp_opp: creal.
-
-Lemma Ropp_mult_distr_r : forall r1 r2, - (r1 * r2) == r1 * - r2.
-Proof.
-  intros; ring.
-Qed.
-
-Lemma Ropp_mult_distr_r_reverse : forall r1 r2, r1 * - r2 == - (r1 * r2).
-Proof.
-  intros; ring.
-Qed.
-
-(*********************************************************)
-(** ** Subtraction                                      *)
-(*********************************************************)
-
-Lemma Rminus_0_r : forall r, r - 0 == r.
-Proof.
-  intro r. unfold Rminus. ring.
-Qed.
-Hint Resolve Rminus_0_r: creal.
-
-Lemma Rminus_0_l : forall r, 0 - r == - r.
-Proof.
-  intro r. unfold Rminus. ring.
-Qed.
-Hint Resolve Rminus_0_l: creal.
-
-(**********)
-Lemma Ropp_minus_distr : forall r1 r2, - (r1 - r2) == r2 - r1.
-Proof.
-  intros; ring.
-Qed.
-Hint Resolve Ropp_minus_distr: creal.
-
-Lemma Ropp_minus_distr' : forall r1 r2, - (r2 - r1) == r1 - r2.
-Proof.
-  intros; ring.
-Qed.
-
-(**********)
-Lemma Rminus_diag_eq : forall r1 r2, r1 == r2 -> r1 - r2 == 0.
-Proof.
-  intros; rewrite H; unfold Rminus; ring.
-Qed.
-Hint Resolve Rminus_diag_eq: creal.
-
-(**********)
-Lemma Rminus_diag_uniq : forall r1 r2, r1 - r2 == 0 -> r1 == r2.
-Proof.
-  intros r1 r2. unfold Rminus,CRminus; rewrite Rplus_comm; intro.
-  rewrite <- (Ropp_involutive r2); apply (Rplus_opp_r_uniq (- r2) r1 H).
-Qed.
-Hint Immediate Rminus_diag_uniq: creal.
-
-Lemma Rminus_diag_uniq_sym : forall r1 r2, r2 - r1 == 0 -> r1 == r2.
-Proof.
-  intros; generalize (Rminus_diag_uniq r2 r1 H); clear H;
-    intro H; rewrite H; reflexivity.
-Qed.
-Hint Immediate Rminus_diag_uniq_sym: creal.
-
-Lemma Rplus_minus : forall r1 r2, r1 + (r2 - r1) == r2.
-Proof.
-  intros; ring.
-Qed.
-Hint Resolve Rplus_minus: creal.
-
-(**********)
-Lemma Rmult_minus_distr_l :
-  forall r1 r2 r3, r1 * (r2 - r3) == r1 * r2 - r1 * r3.
-Proof.
-  intros; ring.
-Qed.
-
-
-(*********************************************************)
-(** ** Order and addition                                *)
-(*********************************************************)
-
-(** *** Compatibility *)
-
-(** Remark: [Rplus_lt_compat_l] is an axiom *)
-
-Lemma Rplus_gt_compat_l : forall r r1 r2, r1 > r2 -> r + r1 > r + r2.
-Proof.
-  intros. apply Rplus_lt_compat_l. apply H.
-Qed.
-Hint Resolve Rplus_gt_compat_l: creal.
-
-(**********)
-Lemma Rplus_lt_compat_r : forall r r1 r2, r1 < r2 -> r1 + r < r2 + r.
-Proof.
-  intros.
-  rewrite (Rplus_comm r1 r); rewrite (Rplus_comm r2 r).
-  apply Rplus_lt_compat_l. exact H.
-Qed.
-Hint Resolve Rplus_lt_compat_r: creal.
-
-Lemma Rplus_gt_compat_r : forall r r1 r2, r1 > r2 -> r1 + r > r2 + r.
-Proof. do 3 intro; apply Rplus_lt_compat_r. Qed.
-
-(**********)
-
-Lemma Rplus_lt_reg_r : forall r r1 r2, r1 + r < r2 + r -> r1 < r2.
-Proof.
-  intros.
-  apply (Rplus_lt_reg_l r).
-  now rewrite 2!(Rplus_comm r).
-Qed.
-
-Lemma Rplus_le_compat_l : forall r r1 r2, r1 <= r2 -> r + r1 <= r + r2.
-Proof.
-  intros. intro abs. apply Rplus_lt_reg_l in abs. contradiction.
-Qed.
-
-Lemma Rplus_ge_compat_l : forall r r1 r2, r1 >= r2 -> r + r1 >= r + r2.
-Proof.
-  intros. apply Rplus_le_compat_l. apply H.
-Qed.
-Hint Resolve Rplus_ge_compat_l: creal.
-
-(**********)
-Lemma Rplus_le_compat_r : forall r r1 r2, r1 <= r2 -> r1 + r <= r2 + r.
-Proof.
-  intros. intro abs. apply Rplus_lt_reg_r in abs. contradiction.
-Qed.
-
-Hint Resolve Rplus_le_compat_l Rplus_le_compat_r: creal.
-
-Lemma Rplus_ge_compat_r : forall r r1 r2, r1 >= r2 -> r1 + r >= r2 + r.
-Proof.
-  intros. apply Rplus_le_compat_r. apply H.
-Qed.
-
-(*********)
-Lemma Rplus_lt_compat :
-  forall r1 r2 r3 r4, r1 < r2 -> r3 < r4 -> r1 + r3 < r2 + r4.
-Proof.
-  intros; apply Rlt_trans with (r2 + r3); auto with creal.
-Qed.
-Hint Immediate Rplus_lt_compat: creal.
-
-Lemma Rplus_le_compat :
-  forall r1 r2 r3 r4, r1 <= r2 -> r3 <= r4 -> r1 + r3 <= r2 + r4.
-Proof.
-  intros; apply Rle_trans with (r2 + r3); auto with creal.
-Qed.
-Hint Immediate Rplus_le_compat: creal.
-
-Lemma Rplus_gt_compat :
-  forall r1 r2 r3 r4, r1 > r2 -> r3 > r4 -> r1 + r3 > r2 + r4.
-Proof.
-  intros. apply Rplus_lt_compat; assumption.
-Qed.
-
-Lemma Rplus_ge_compat :
-  forall r1 r2 r3 r4, r1 >= r2 -> r3 >= r4 -> r1 + r3 >= r2 + r4.
-Proof.
-  intros. apply Rplus_le_compat; assumption.
-Qed.
-
-(*********)
-Lemma Rplus_lt_le_compat :
-  forall r1 r2 r3 r4, r1 < r2 -> r3 <= r4 -> r1 + r3 < r2 + r4.
-Proof.
-  intros; apply Rlt_le_trans with (r2 + r3); auto with creal.
-Qed.
-
-Lemma Rplus_le_lt_compat :
-  forall r1 r2 r3 r4, r1 <= r2 -> r3 < r4 -> r1 + r3 < r2 + r4.
-Proof.
-  intros; apply Rle_lt_trans with (r2 + r3); auto with creal.
-Qed.
-
-Hint Immediate Rplus_lt_le_compat Rplus_le_lt_compat: creal.
-
-Lemma Rplus_gt_ge_compat :
-  forall r1 r2 r3 r4, r1 > r2 -> r3 >= r4 -> r1 + r3 > r2 + r4.
-Proof.
-  intros. apply Rplus_lt_le_compat; assumption.
-Qed.
-
-Lemma Rplus_ge_gt_compat :
-  forall r1 r2 r3 r4, r1 >= r2 -> r3 > r4 -> r1 + r3 > r2 + r4.
-Proof.
-  intros. apply Rplus_le_lt_compat; assumption.
-Qed.
-
-(**********)
-Lemma Rplus_lt_0_compat : forall r1 r2, 0 < r1 -> 0 < r2 -> 0 < r1 + r2.
-Proof.
-  intros. apply (Rlt_trans _ (r1+0)). rewrite Rplus_0_r. exact H.
-  apply Rplus_lt_compat_l. exact H0.
-Qed.
-
-Lemma Rplus_le_lt_0_compat : forall r1 r2, 0 <= r1 -> 0 < r2 -> 0 < r1 + r2.
-Proof.
-  intros. apply (Rle_lt_trans _ (r1+0)). rewrite Rplus_0_r. exact H.
-  apply Rplus_lt_compat_l. exact H0.
-Qed.
-
-Lemma Rplus_lt_le_0_compat : forall r1 r2, 0 < r1 -> 0 <= r2 -> 0 < r1 + r2.
-Proof.
-  intros x y; intros; rewrite <- Rplus_comm; apply Rplus_le_lt_0_compat;
-    assumption.
-Qed.
-
-Lemma Rplus_le_le_0_compat : forall r1 r2, 0 <= r1 -> 0 <= r2 -> 0 <= r1 + r2.
-Proof.
-  intros. apply (Rle_trans _ (r1+0)). rewrite Rplus_0_r. exact H.
-  apply Rplus_le_compat_l. exact H0.
-Qed.
-
-(**********)
-Lemma sum_inequa_Rle_lt :
-  forall a x b c y d,
-    a <= x -> x < b -> c < y -> y <= d -> a + c < x + y < b + d.
-Proof.
-  intros; split.
-  apply Rlt_le_trans with (a + y); auto with creal.
-  apply Rlt_le_trans with (b + y); auto with creal.
-Qed.
-
-(** *** Cancellation *)
-
-Lemma Rplus_le_reg_l : forall r r1 r2, r + r1 <= r + r2 -> r1 <= r2.
-Proof.
-  intros. intro abs. apply (Rplus_lt_compat_l r) in abs. contradiction.
-Qed.
-
-Lemma Rplus_le_reg_r : forall r r1 r2, r1 + r <= r2 + r -> r1 <= r2.
-Proof.
-  intros.
-  apply (Rplus_le_reg_l r).
-  now rewrite 2!(Rplus_comm r).
-Qed.
-
-Lemma Rplus_gt_reg_l : forall r r1 r2, r + r1 > r + r2 -> r1 > r2.
-Proof.
-  unfold CRealGt; intros; apply (Rplus_lt_reg_l r r2 r1 H).
-Qed.
-
-Lemma Rplus_ge_reg_l : forall r r1 r2, r + r1 >= r + r2 -> r1 >= r2.
-Proof.
-  intros; apply Rle_ge; apply Rplus_le_reg_l with r; auto with creal.
-Qed.
-
-(**********)
-Lemma Rplus_le_reg_pos_r :
-  forall r1 r2 r3, 0 <= r2 -> r1 + r2 <= r3 -> r1 <= r3.
-Proof.
-  intros. apply (Rle_trans _ (r1+r2)). 2: exact H0.
-  rewrite <- (Rplus_0_r r1), Rplus_assoc.
-  apply Rplus_le_compat_l. rewrite Rplus_0_l. exact H.
-Qed.
-
-Lemma Rplus_lt_reg_pos_r : forall r1 r2 r3, 0 <= r2 -> r1 + r2 < r3 -> r1 < r3.
-Proof.
-  intros. apply (Rle_lt_trans _ (r1+r2)). 2: exact H0.
-  rewrite <- (Rplus_0_r r1), Rplus_assoc.
-  apply Rplus_le_compat_l. rewrite Rplus_0_l. exact H.
-Qed.
-
-Lemma Rplus_ge_reg_neg_r :
-  forall r1 r2 r3, 0 >= r2 -> r1 + r2 >= r3 -> r1 >= r3.
-Proof.
-  intros. apply (Rge_trans _ (r1+r2)). 2: exact H0.
-  apply Rle_ge. rewrite <- (Rplus_0_r r1), Rplus_assoc.
-  apply Rplus_le_compat_l. rewrite Rplus_0_l. exact H.
-Qed.
-
-Lemma Rplus_gt_reg_neg_r : forall r1 r2 r3, 0 >= r2 -> r1 + r2 > r3 -> r1 > r3.
-Proof.
-  intros. apply (Rlt_le_trans _ (r1+r2)). exact H0.
-  rewrite <- (Rplus_0_r r1), Rplus_assoc.
-  apply Rplus_le_compat_l. rewrite Rplus_0_l. exact H.
-Qed.
-
-(***********)
-Lemma Rplus_eq_0_l :
-  forall r1 r2, 0 <= r1 -> 0 <= r2 -> r1 + r2 == 0 -> r1 == 0.
-Proof.
-  intros. split.
-  - intro abs. rewrite <- (Rplus_opp_r r1) in H1.
-    apply Rplus_eq_reg_l in H1. rewrite H1 in H0. clear H1.
-    apply (Rplus_le_compat_l r1) in H0.
-    rewrite Rplus_opp_r in H0. rewrite Rplus_0_r in H0.
-    contradiction.
-  - intro abs. clear H. rewrite <- (Rplus_opp_r r1) in H1.
-    apply Rplus_eq_reg_l in H1. rewrite H1 in H0. clear H1.
-    apply (Rplus_le_compat_l r1) in H0.
-    rewrite Rplus_opp_r in H0. rewrite Rplus_0_r in H0.
-    contradiction.
-Qed.
-
-Lemma Rplus_eq_R0 :
-  forall r1 r2, 0 <= r1 -> 0 <= r2 -> r1 + r2 == 0 -> r1 == 0 /\ r2 == 0.
-Proof.
-  intros a b; split.
-  apply Rplus_eq_0_l with b; auto with creal.
-  apply Rplus_eq_0_l with a; auto with creal.
-  rewrite Rplus_comm; auto with creal.
-Qed.
-
-
-(*********************************************************)
-(** ** Order and opposite                                *)
-(*********************************************************)
-
-(** *** Contravariant compatibility *)
-
-Lemma Ropp_gt_lt_contravar : forall r1 r2, r1 > r2 -> - r1 < - r2.
-Proof.
-  unfold CRealGt; intros.
-  apply (Rplus_lt_reg_l (r2 + r1)).
-  setoid_replace (r2 + r1 + - r1) with r2 by ring.
-  setoid_replace (r2 + r1 + - r2) with r1 by ring.
-  exact H.
-Qed.
-Hint Resolve Ropp_gt_lt_contravar : creal.
-
-Lemma Ropp_lt_gt_contravar : forall r1 r2, r1 < r2 -> - r1 > - r2.
-Proof.
-  intros. apply Ropp_gt_lt_contravar. exact H.
-Qed.
-Hint Resolve Ropp_lt_gt_contravar: creal.
-
-(**********)
-Lemma Ropp_lt_contravar : forall r1 r2, r2 < r1 -> - r1 < - r2.
-Proof.
-  auto with creal.
-Qed.
-Hint Resolve Ropp_lt_contravar: creal.
-
-Lemma Ropp_gt_contravar : forall r1 r2, r2 > r1 -> - r1 > - r2.
-Proof. auto with creal. Qed.
-
-(**********)
-
-Lemma Ropp_lt_cancel : forall r1 r2, - r2 < - r1 -> r1 < r2.
-Proof.
-  intros x y H'.
-  rewrite <- (Ropp_involutive x); rewrite <- (Ropp_involutive y);
-    auto with creal.
-Qed.
-Hint Immediate Ropp_lt_cancel: creal.
-
-Lemma Ropp_gt_cancel : forall r1 r2, - r2 > - r1 -> r1 > r2.
-Proof.
-  intros. apply Ropp_lt_cancel. apply H.
-Qed.
-
-Lemma Ropp_le_ge_contravar : forall r1 r2, r1 <= r2 -> - r1 >= - r2.
-Proof.
-  intros. intro abs. apply Ropp_lt_cancel in abs. contradiction.
-Qed.
-Hint Resolve Ropp_le_ge_contravar: creal.
-
-Lemma Ropp_ge_le_contravar : forall r1 r2, r1 >= r2 -> - r1 <= - r2.
-Proof.
-  intros. intro abs. apply Ropp_lt_cancel in abs. contradiction.
-Qed.
-Hint Resolve Ropp_ge_le_contravar: creal.
-
-(**********)
-Lemma Ropp_le_contravar : forall r1 r2, r2 <= r1 -> - r1 <= - r2.
-Proof.
-  intros. intro abs. apply Ropp_lt_cancel in abs. contradiction.
-Qed.
-Hint Resolve Ropp_le_contravar: creal.
-
-Lemma Ropp_ge_contravar : forall r1 r2, r2 >= r1 -> - r1 >= - r2.
-Proof.
-  intros. apply Ropp_le_contravar. apply H.
-Qed.
-
-(**********)
-Lemma Ropp_0_lt_gt_contravar : forall r, 0 < r -> 0 > - r.
-Proof.
-  intros; setoid_replace 0 with (-0); auto with creal. ring.
-Qed.
-Hint Resolve Ropp_0_lt_gt_contravar: creal.
-
-Lemma Ropp_0_gt_lt_contravar : forall r, 0 > r -> 0 < - r.
-Proof.
-  intros; setoid_replace 0 with (-0); auto with creal. ring.
-Qed.
-Hint Resolve Ropp_0_gt_lt_contravar: creal.
-
-(**********)
-Lemma Ropp_lt_gt_0_contravar : forall r, r > 0 -> - r < 0.
-Proof.
-  intros; rewrite <- Ropp_0; auto with creal.
-Qed.
-Hint Resolve Ropp_lt_gt_0_contravar: creal.
-
-Lemma Ropp_gt_lt_0_contravar : forall r, r < 0 -> - r > 0.
-Proof.
-  intros; rewrite <- Ropp_0; auto with creal.
-Qed.
-Hint Resolve Ropp_gt_lt_0_contravar: creal.
-
-(**********)
-Lemma Ropp_0_le_ge_contravar : forall r, 0 <= r -> 0 >= - r.
-Proof.
-  intros; setoid_replace 0 with (-0); auto with creal. ring.
-Qed.
-Hint Resolve Ropp_0_le_ge_contravar: creal.
-
-Lemma Ropp_0_ge_le_contravar : forall r, 0 >= r -> 0 <= - r.
-Proof.
-  intros; setoid_replace 0 with (-0); auto with creal. ring.
-Qed.
-Hint Resolve Ropp_0_ge_le_contravar: creal.
-
-(** *** Cancellation *)
-
-Lemma Ropp_le_cancel : forall r1 r2, - r2 <= - r1 -> r1 <= r2.
-Proof.
-  intros. intro abs. apply Ropp_lt_gt_contravar in abs. contradiction.
-Qed.
-Hint Immediate Ropp_le_cancel: creal.
-
-Lemma Ropp_ge_cancel : forall r1 r2, - r2 >= - r1 -> r1 >= r2.
-Proof.
-  intros. apply Ropp_le_cancel. apply H.
-Qed.
-
-(*********************************************************)
-(** ** Order and multiplication                          *)
-(*********************************************************)
-
-(** Remark: [Rmult_lt_compat_l] is an axiom *)
-
-(** *** Covariant compatibility *)
-
-Lemma Rmult_lt_compat_r : forall r r1 r2, 0 < r -> r1 < r2 -> r1 * r < r2 * r.
-Proof.
-  intros; rewrite (Rmult_comm r1 r); rewrite (Rmult_comm r2 r); auto with creal.
-Qed.
-Hint Resolve Rmult_lt_compat_r : core.
-
-Lemma Rmult_gt_compat_r : forall r r1 r2, r > 0 -> r1 > r2 -> r1 * r > r2 * r.
-Proof.
-  intros. apply Rmult_lt_compat_r; assumption.
-Qed.
-
-Lemma Rmult_gt_compat_l : forall r r1 r2, r > 0 -> r1 > r2 -> r * r1 > r * r2.
-Proof.
-  intros. apply Rmult_lt_compat_l; assumption.
-Qed.
-
-Lemma Rmult_gt_0_lt_compat :
-  forall r1 r2 r3 r4,
-    r3 > 0 -> r2 > 0 -> r1 < r2 -> r3 < r4 -> r1 * r3 < r2 * r4.
-Proof.
-  intros; apply Rlt_trans with (r2 * r3); auto with creal.
-Qed.
-
-(*********)
-Lemma Rmult_lt_0_compat : forall r1 r2, 0 < r1 -> 0 < r2 -> 0 < r1 * r2.
-Proof.
-  intros; setoid_replace 0 with (0 * r2); auto with creal.
-  rewrite Rmult_0_l. reflexivity.
-Qed.
-
-Lemma Rmult_gt_0_compat : forall r1 r2, r1 > 0 -> r2 > 0 -> r1 * r2 > 0.
-Proof.
-  apply Rmult_lt_0_compat.
-Qed.
-
-(** *** Contravariant compatibility *)
-
-Lemma Rmult_lt_gt_compat_neg_l :
-  forall r r1 r2, r < 0 -> r1 < r2 -> r * r1 > r * r2.
-Proof.
-  intros; setoid_replace r with (- - r); auto with creal.
-  rewrite (Ropp_mult_distr_l_reverse (- r));
-    rewrite (Ropp_mult_distr_l_reverse (- r)).
-  apply Ropp_lt_gt_contravar; auto with creal.
-  rewrite Ropp_involutive. reflexivity.
-Qed.
-
-(** *** Cancellation *)
-
-Lemma Rinv_0_lt_compat : forall r (rpos : 0 < r), 0 < (/ r) (inr rpos).
-Proof.
-  intros. apply CRinv_0_lt_compat. exact rpos.
-Qed.
-
-Lemma Rmult_lt_reg_l : forall r r1 r2, 0 < r -> r * r1 < r * r2 -> r1 < r2.
-Proof.
-  intros z x y H H0.
-  apply (Rmult_lt_compat_l ((/z) (inr H))) in H0.
-  repeat rewrite <- Rmult_assoc in H0. rewrite Rinv_l in H0.
-  repeat rewrite Rmult_1_l in H0. apply H0.
-  apply Rinv_0_lt_compat.
-Qed.
-
-Lemma Rmult_lt_reg_r : forall r r1 r2, 0 < r -> r1 * r < r2 * r -> r1 < r2.
-Proof.
-  intros.
-  apply Rmult_lt_reg_l with r.
-  exact H.
-  now rewrite 2!(Rmult_comm r).
-Qed.
-
-Lemma Rmult_gt_reg_l : forall r r1 r2, 0 < r -> r * r1 < r * r2 -> r1 < r2.
-Proof.
-  intros. apply Rmult_lt_reg_l in H0; assumption.
-Qed.
-
-Lemma Rmult_le_reg_l : forall r r1 r2, 0 < r -> r * r1 <= r * r2 -> r1 <= r2.
-Proof.
-  intros. intro abs. apply (Rmult_lt_compat_l r) in abs.
-  contradiction. apply H.
-Qed.
-
-Lemma Rmult_le_reg_r : forall r r1 r2, 0 < r -> r1 * r <= r2 * r -> r1 <= r2.
-Proof.
-  intros.
-  apply Rmult_le_reg_l with r.
-  exact H.
-  now rewrite 2!(Rmult_comm r).
-Qed.
-
-(*********************************************************)
-(** ** Order and substraction                            *)
-(*********************************************************)
-
-Lemma Rlt_minus : forall r1 r2, r1 < r2 -> r1 - r2 < 0.
-Proof.
-  intros; apply (Rplus_lt_reg_l r2).
-  setoid_replace (r2 + (r1 - r2)) with r1 by ring.
-  now rewrite Rplus_0_r.
-Qed.
-Hint Resolve Rlt_minus: creal.
-
-Lemma Rgt_minus : forall r1 r2, r1 > r2 -> r1 - r2 > 0.
-Proof.
-  intros; apply (Rplus_lt_reg_l r2).
-  setoid_replace (r2 + (r1 - r2)) with r1 by ring.
-  now rewrite Rplus_0_r.
-Qed.
-
-Lemma Rlt_Rminus : forall a b, a < b -> 0 < b - a.
-Proof.
-  intros a b; apply Rgt_minus.
-Qed.
-
-(**********)
-Lemma Rle_minus : forall r1 r2, r1 <= r2 -> r1 - r2 <= 0.
-Proof.
-  intros. intro abs. apply (Rplus_lt_compat_l r2) in abs.
-  unfold Rminus in abs.
-  rewrite Rplus_0_r, Rplus_comm, Rplus_assoc, Rplus_opp_l, Rplus_0_r in abs.
-  contradiction.
-Qed.
-
-Lemma Rge_minus : forall r1 r2, r1 >= r2 -> r1 - r2 >= 0.
-Proof.
-  intros. intro abs. apply (Rplus_lt_compat_l r2) in abs.
-  unfold Rminus in abs.
-  rewrite Rplus_0_r, Rplus_comm, Rplus_assoc, Rplus_opp_l, Rplus_0_r in abs.
-  contradiction.
-Qed.
-
-(**********)
-Lemma Rminus_lt : forall r1 r2, r1 - r2 < 0 -> r1 < r2.
-Proof.
-  intros. rewrite <- (Rplus_opp_r r2) in H.
-  apply Rplus_lt_reg_r in H. exact H.
-Qed.
-
-Lemma Rminus_gt : forall r1 r2, r1 - r2 > 0 -> r1 > r2.
-Proof.
-  intros. rewrite <- (Rplus_opp_r r2) in H.
-  apply Rplus_lt_reg_r in H. exact H.
-Qed.
-
-Lemma Rminus_gt_0_lt : forall a b, 0 < b - a -> a < b.
-Proof. intro; intro; apply Rminus_gt. Qed.
-
-(**********)
-Lemma Rminus_le : forall r1 r2, r1 - r2 <= 0 -> r1 <= r2.
-Proof.
-  intros. rewrite <- (Rplus_opp_r r2) in H.
-  apply Rplus_le_reg_r in H. exact H.
-Qed.
-
-Lemma Rminus_ge : forall r1 r2, r1 - r2 >= 0 -> r1 >= r2.
-Proof.
-  intros. rewrite <- (Rplus_opp_r r2) in H.
-  apply Rplus_le_reg_r in H. exact H.
-Qed.
-
-(**********)
-Lemma tech_Rplus : forall r s, 0 <= r -> 0 < s -> r + s <> 0.
-Proof.
-  intros; apply not_eq_sym; apply Rlt_not_eq.
-  rewrite Rplus_comm; setoid_replace 0 with (0 + 0); auto with creal. ring.
-Qed.
-Hint Immediate tech_Rplus: creal.
-
-(*********************************************************)
-(** ** Zero is less than one                             *)
-(*********************************************************)
-
-Lemma Rle_0_1 : 0 <= 1.
-Proof.
-  intro abs. apply (Rlt_asym 0 1).
-  apply Rlt_0_1. apply abs.
-Qed.
-
-
-(*********************************************************)
-(** ** Inverse                                           *)
-(*********************************************************)
-
-Lemma Rinv_1 : forall nz : 1 # 0, (/ 1) nz == 1.
-Proof.
-  intros. rewrite <- (Rmult_1_l ((/1) nz)). rewrite Rinv_r.
-  reflexivity. right. apply Rlt_0_1.
-Qed.
-Hint Resolve Rinv_1: creal.
-
-(*********)
-Lemma Ropp_inv_permute : forall r (rnz : r # 0) (ronz : (-r) # 0),
-    - (/ r) rnz == (/ - r) ronz.
-Proof.
-  intros.
-  apply (Rmult_eq_reg_l (-r)). rewrite Rinv_r.
-  rewrite <- Ropp_mult_distr_l. rewrite <- Ropp_mult_distr_r.
-  rewrite Ropp_involutive. rewrite Rinv_r. reflexivity.
-  exact rnz. exact ronz. exact ronz.
-Qed.
-
-(*********)
-Lemma Rinv_neq_0_compat : forall r (rnz : r # 0), ((/ r) rnz) # 0.
-Proof.
-  intros. destruct rnz. left.
-  assert (0 < (/-r) (inr (Ropp_0_gt_lt_contravar _ c))).
-  { apply Rinv_0_lt_compat. }
-  rewrite <- (Ropp_inv_permute _ (inl c)) in H.
-  apply Ropp_lt_cancel. rewrite Ropp_0. exact H.
-  right. apply Rinv_0_lt_compat.
-Qed.
-Hint Resolve Rinv_neq_0_compat: creal.
-
-(*********)
-Lemma Rinv_involutive : forall r (rnz : r # 0) (rinz : ((/ r) rnz) # 0),
-    (/ ((/ r) rnz)) rinz == r.
-Proof.
-  intros. apply (Rmult_eq_reg_l ((/r) rnz)). rewrite Rinv_r.
-  rewrite Rinv_l. reflexivity. exact rinz. exact rinz.
-Qed.
-Hint Resolve Rinv_involutive: creal.
-
-(*********)
-Lemma Rinv_mult_distr :
-  forall r1 r2 (r1nz : r1 # 0) (r2nz : r2 # 0) (rmnz : (r1*r2) # 0),
-    (/ (r1 * r2)) rmnz == (/ r1) r1nz * (/ r2) r2nz.
-Proof.
-  intros. apply (Rmult_eq_reg_l r1). 2: exact r1nz.
-  rewrite <- Rmult_assoc. rewrite Rinv_r. rewrite Rmult_1_l.
-  apply (Rmult_eq_reg_l r2). 2: exact r2nz.
-  rewrite Rinv_r. rewrite <- Rmult_assoc.
-  rewrite (Rmult_comm r2 r1). rewrite Rinv_r.
-  reflexivity. exact rmnz. exact r2nz. exact r1nz.
-Qed.
-
-Lemma Rinv_r_simpl_r : forall r1 r2 (rnz : r1 # 0), r1 * (/ r1) rnz * r2 == r2.
-Proof.
-  intros; transitivity (1 * r2); auto with creal.
-  rewrite Rinv_r; auto with creal. rewrite Rmult_1_l. reflexivity.
-Qed.
-
-Lemma Rinv_r_simpl_l : forall r1 r2 (rnz : r1 # 0),
-    r2 * r1 * (/ r1) rnz == r2.
-Proof.
-  intros. rewrite Rmult_assoc. rewrite Rinv_r, Rmult_1_r.
-  reflexivity. exact rnz.
-Qed.
-
-Lemma Rinv_r_simpl_m : forall r1 r2 (rnz : r1 # 0),
-    r1 * r2 * (/ r1) rnz == r2.
-Proof.
-  intros. rewrite Rmult_comm, <- Rmult_assoc, Rinv_l, Rmult_1_l.
-  reflexivity.
-Qed.
-Hint Resolve Rinv_r_simpl_l Rinv_r_simpl_r Rinv_r_simpl_m: creal.
-
-(*********)
-Lemma Rinv_mult_simpl :
-  forall r1 r2 r3 (r1nz : r1 # 0) (r2nz : r2 # 0),
-    r1 * (/ r2) r2nz * (r3 * (/ r1) r1nz) == r3 * (/ r2) r2nz.
-Proof.
-  intros a b c; intros.
-  transitivity (a * (/ a) r1nz * (c * (/ b) r2nz)); auto with creal.
-  ring.
-Qed.
-
-Lemma Rinv_eq_compat : forall x y (rxnz : x # 0) (rynz : y # 0),
-    x == y
-    -> (/ x) rxnz == (/ y) rynz.
-Proof.
-  intros. apply (Rmult_eq_reg_l x). rewrite Rinv_r.
-  rewrite H. rewrite Rinv_r. reflexivity.
-  exact rynz. exact rxnz. exact rxnz.
-Qed.
-
-
-(*********************************************************)
-(** ** Order and inverse                                 *)
-(*********************************************************)
-
-Lemma Rinv_lt_0_compat : forall r (rneg : r < 0), (/ r) (inl rneg) < 0.
-Proof.
-  intros. assert (0 < (/-r) (inr (Ropp_0_gt_lt_contravar r rneg))).
-  { apply Rinv_0_lt_compat. }
-  rewrite <- Ropp_inv_permute in H. rewrite <- Ropp_0 in H.
-  apply Ropp_lt_cancel in H. apply H.
-Qed.
-Hint Resolve Rinv_lt_0_compat: creal.
-
-
-
-(*********************************************************)
-(** ** Miscellaneous                                     *)
-(*********************************************************)
-
-(**********)
-Lemma Rle_lt_0_plus_1 : forall r, 0 <= r -> 0 < r + 1.
-Proof.
-  intros. apply (Rle_lt_trans _ (r+0)). rewrite Rplus_0_r.
-  exact H. apply Rplus_lt_compat_l. apply Rlt_0_1.
-Qed.
-Hint Resolve Rle_lt_0_plus_1: creal.
-
-(**********)
-Lemma Rlt_plus_1 : forall r, r < r + 1.
-Proof.
-  intro r. rewrite <- Rplus_0_r. rewrite Rplus_assoc.
-  apply Rplus_lt_compat_l. rewrite Rplus_0_l. exact Rlt_0_1.
-Qed.
-Hint Resolve Rlt_plus_1: creal.
-
-(**********)
-Lemma tech_Rgt_minus : forall r1 r2, 0 < r2 -> r1 > r1 - r2.
-Proof.
-  intros. apply (Rplus_lt_reg_r r2).
-  unfold Rminus, CRminus; rewrite Rplus_assoc, Rplus_opp_l.
-  apply Rplus_lt_compat_l. exact H.
-Qed.
-
-(*********************************************************)
-(** ** Injection from [N] to [R]                         *)
-(*********************************************************)
-
-(**********)
-Lemma S_INR : forall n:nat, INR (S n) == INR n + 1.
-Proof.
-  intro; destruct n. rewrite Rplus_0_l. reflexivity. reflexivity.
-Qed.
-
-(**********)
-Lemma IZN : forall n:Z, (0 <= n)%Z -> { m : nat | n = Z.of_nat m }.
-Proof.
-  intros. exists (Z.to_nat n). rewrite Z2Nat.id. reflexivity. assumption.
-Qed.
-
-Lemma le_succ_r_T : forall n m : nat, (n <= S m)%nat -> {(n <= m)%nat} + {n = S m}.
-Proof.
-  intros. destruct (le_lt_dec n m). left. exact l.
-  right. apply Nat.le_succ_r in H. destruct H.
-  exfalso. apply (le_not_lt n m); assumption. exact H.
-Qed.
-
-Lemma lt_INR : forall n m:nat, (n < m)%nat -> INR n < INR m.
-Proof.
-  induction m.
-  - intros. exfalso. inversion H.
-  - intros. unfold lt in H. apply le_S_n in H. destruct m.
-    assert (n = 0)%nat.
-    { inversion H. reflexivity. }
-    subst n. apply Rlt_0_1. apply le_succ_r_T in H. destruct H.
-    rewrite S_INR. apply (Rlt_trans _ (INR (S m) + 0)).
-    rewrite Rplus_comm, Rplus_0_l. apply IHm.
-    apply le_n_S. exact l.
-    apply Rplus_lt_compat_l. exact Rlt_0_1.
-    subst n. rewrite (S_INR (S m)). rewrite <- (Rplus_0_l).
-    rewrite (Rplus_comm 0), Rplus_assoc.
-    apply Rplus_lt_compat_l. rewrite Rplus_0_l.
-    exact Rlt_0_1.
-Qed.
-
-(**********)
-Lemma S_O_plus_INR : forall n:nat, INR (1 + n) == INR 1 + INR n.
-Proof.
-  intros; destruct n.
-  - rewrite Rplus_comm, Rplus_0_l. reflexivity.
-  - rewrite Rplus_comm. reflexivity.
-Qed.
-
-(**********)
-Lemma plus_INR : forall n m:nat, INR (n + m) == INR n + INR m.
-Proof.
-  intros n m; induction  n as [| n Hrecn].
-  - rewrite Rplus_0_l. reflexivity.
-  - replace (S n + m)%nat with (S (n + m)); auto with arith.
-    repeat rewrite S_INR.
-    rewrite Hrecn; ring.
-Qed.
-
-(**********)
-Lemma minus_INR : forall n m:nat, (m <= n)%nat -> INR (n - m) == INR n - INR m.
-Proof.
-  intros n m le; pattern m, n; apply le_elim_rel.
-  intros. rewrite <- minus_n_O. simpl.
-  unfold Rminus, CRminus. rewrite Ropp_0, Rplus_0_r. reflexivity.
-  intros; repeat rewrite S_INR; simpl.
-  rewrite H0. unfold Rminus. ring. exact le.
-Qed.
-
-(*********)
-Lemma mult_INR : forall n m:nat, INR (n * m) == INR n * INR m.
-Proof.
-  intros n m; induction  n as [| n Hrecn].
-  - rewrite Rmult_0_l. reflexivity.
-  - intros; repeat rewrite S_INR; simpl.
-    rewrite plus_INR. rewrite Hrecn; ring.
-Qed.
-
-Lemma INR_IPR : forall p, INR (Pos.to_nat p) == IPR p.
-Proof.
-  assert (H: forall p, 2 * INR (Pos.to_nat p) == IPR_2 p).
-  { induction p as [p|p|].
-    - unfold IPR_2; rewrite Pos2Nat.inj_xI, S_INR, mult_INR, <- IHp.
-      rewrite Rplus_comm. reflexivity.
-    - unfold IPR_2; now rewrite Pos2Nat.inj_xO, mult_INR, <- IHp.
-    - apply Rmult_1_r. }
-  intros [p|p|] ; unfold IPR.
-  rewrite Pos2Nat.inj_xI, S_INR, mult_INR, <- H.
-  apply Rplus_comm.
-  now rewrite Pos2Nat.inj_xO, mult_INR, <- H.
-  easy.
-Qed.
-
-Fixpoint pow (r:R) (n:nat) : R :=
-  match n with
-    | O => 1
-    | S n => r * (pow r n)
-  end.
-
-Lemma Rpow_eq_compat : forall (x y : R) (n : nat),
-    x == y -> pow x n == pow y n.
-Proof.
-  intro x. induction n.
-  - reflexivity.
-  - intros. simpl. rewrite IHn, H. reflexivity. exact H.
-Qed.
-
-Lemma pow_INR (m n: nat) :  INR (m ^ n) == pow (INR m) n.
-Proof. now induction n as [|n IHn];[ | simpl; rewrite mult_INR, IHn]. Qed.
-
-(*********)
-Lemma lt_0_INR : forall n:nat, (0 < n)%nat -> 0 < INR n.
-Proof.
-  intros. apply (lt_INR 0). exact H.
-Qed.
-Hint Resolve lt_0_INR: creal.
-
-Lemma lt_1_INR : forall n:nat, (1 < n)%nat -> 1 < INR n.
-Proof.
-  apply lt_INR.
-Qed.
-Hint Resolve lt_1_INR: creal.
-
-(**********)
-Lemma pos_INR_nat_of_P : forall p:positive, 0 < INR (Pos.to_nat p).
-Proof.
-  intro; apply lt_0_INR.
-  simpl; auto with creal.
-  apply Pos2Nat.is_pos.
-Qed.
-Hint Resolve pos_INR_nat_of_P: creal.
-
-(**********)
-Lemma pos_INR : forall n:nat, 0 <= INR n.
-Proof.
-  intro n; case n.
-  simpl; auto with creal.
-  auto with arith creal.
-Qed.
-Hint Resolve pos_INR: creal.
-
-Lemma INR_lt : forall n m:nat, INR n < INR m -> (n < m)%nat.
-Proof.
-  intros n m. revert n.
-  induction m ; intros n H.
-  - elim (Rlt_irrefl 0).
-    apply Rle_lt_trans with (2 := H).
-    apply pos_INR.
-  - destruct n as [|n].
-    apply Nat.lt_0_succ.
-    apply lt_n_S, IHm.
-    rewrite 2!S_INR in H.
-    apply Rplus_lt_reg_r with (1 := H).
-Qed.
-Hint Resolve INR_lt: creal.
-
-(*********)
-Lemma le_INR : forall n m:nat, (n <= m)%nat -> INR n <= INR m.
-Proof.
-  simple induction 1; intros; auto with creal.
-  rewrite S_INR.
-  apply Rle_trans with (INR m0); auto with creal.
-Qed.
-Hint Resolve le_INR: creal.
-
-(**********)
-Lemma INR_not_0 : forall n:nat, INR n <> 0 -> n <> 0%nat.
-Proof.
-  red; intros n H H1.
-  apply H.
-  rewrite H1; trivial.
-Qed.
-Hint Immediate INR_not_0: creal.
-
-(**********)
-Lemma not_0_INR : forall n:nat, n <> 0%nat -> 0 < INR n.
-Proof.
-  intro n; case n.
-  intro; absurd (0%nat = 0%nat); trivial.
-  intros; rewrite S_INR.
-  apply (Rlt_le_trans _ (0 + 1)). rewrite Rplus_0_l. apply Rlt_0_1.
-  apply Rplus_le_compat_r. apply pos_INR.
-Qed.
-Hint Resolve not_0_INR: creal.
-
-Lemma not_INR : forall n m:nat, n <> m -> INR n # INR m.
-Proof.
-  intros n m H; case (le_lt_dec n m); intros H1.
-  left. apply lt_INR.
-  case (le_lt_or_eq _ _ H1); intros H2.
-  exact H2. contradiction.
-  right. apply lt_INR. exact H1.
-Qed.
-Hint Resolve not_INR: creal.
-
-Lemma INR_eq : forall n m:nat, INR n == INR m -> n = m.
-Proof.
-  intros n m HR.
-  destruct (dec_eq_nat n m) as [H|H].
-  exact H. exfalso.
-  apply not_INR in H. destruct HR,H; contradiction.
-Qed.
-Hint Resolve INR_eq: creal.
-
-Lemma INR_le : forall n m:nat, INR n <= INR m -> (n <= m)%nat.
-Proof.
-  intros n m. revert n.
-  induction m ; intros n H.
-  - destruct n. apply le_refl. exfalso.
-    rewrite S_INR in H.
-    assert (0 + 1 <= 0). apply (Rle_trans _ (INR n + 1)).
-    apply Rplus_le_compat_r. apply pos_INR. apply H.
-    rewrite Rplus_0_l in H0. apply H0. apply Rlt_0_1.
-  - destruct n as [|n]. apply le_0_n.
-    apply le_n_S, IHm.
-    rewrite 2!S_INR in H.
-    apply Rplus_le_reg_r in H. apply H.
-Qed.
-Hint Resolve INR_le: creal.
-
-Lemma not_1_INR : forall n:nat, n <> 1%nat -> INR n # 1.
-Proof.
-  intros n.
-  apply not_INR.
-Qed.
-Hint Resolve not_1_INR: creal.
-
-(*********************************************************)
-(** ** Injection from [Z] to [R]                         *)
-(*********************************************************)
-
-Lemma IPR_pos : forall p:positive, 0 < IPR p.
-Proof.
-  intro p. rewrite <- INR_IPR. apply (lt_INR 0), Pos2Nat.is_pos.
-Qed.
-
-Lemma IPR_double : forall p:positive, IPR (2*p) == 2 * IPR p.
-Proof.
-  intro p. destruct p; try reflexivity.
-  rewrite Rmult_1_r. reflexivity.
-Qed.
-
-Lemma INR_IZR_INZ : forall n:nat, INR n == IZR (Z.of_nat n).
-Proof.
-  intros [|n].
-  easy.
-  simpl Z.of_nat. unfold IZR.
-  now rewrite <- INR_IPR, SuccNat2Pos.id_succ.
-Qed.
-
-Lemma plus_IZR_NEG_POS :
-  forall p q:positive, IZR (Zpos p + Zneg q) == IZR (Zpos p) + IZR (Zneg q).
-Proof.
-  intros p q; simpl. rewrite Z.pos_sub_spec.
-  case Pos.compare_spec; intros H; unfold IZR.
-  subst. ring.
-  rewrite <- 3!INR_IPR, Pos2Nat.inj_sub.
-  rewrite minus_INR.
-  2: (now apply lt_le_weak, Pos2Nat.inj_lt).
-  ring.
-  trivial.
-  rewrite <- 3!INR_IPR, Pos2Nat.inj_sub.
-  rewrite minus_INR.
-  2: (now apply lt_le_weak, Pos2Nat.inj_lt).
-  unfold Rminus. ring. trivial.
-Qed.
-
-Lemma plus_IPR : forall n m:positive, IPR (n + m) == IPR n + IPR m.
-Proof.
-  intros. repeat rewrite <- INR_IPR.
-  rewrite Pos2Nat.inj_add. apply plus_INR.
-Qed.
-
-(**********)
-Lemma plus_IZR : forall n m:Z, IZR (n + m) == IZR n + IZR m.
-Proof.
-  intro z; destruct z; intro t; destruct t; intros.
-  - rewrite Rplus_0_l. reflexivity.
-  - rewrite Rplus_0_l. rewrite Z.add_0_l. reflexivity.
-  - rewrite Rplus_0_l. reflexivity.
-  - rewrite Rplus_comm,Rplus_0_l. reflexivity.
-  - rewrite <- Pos2Z.inj_add. unfold IZR. apply plus_IPR.
-  - apply plus_IZR_NEG_POS.
-  - rewrite Rplus_comm,Rplus_0_l, Z.add_0_r. reflexivity.
-  - rewrite Z.add_comm; rewrite Rplus_comm; apply plus_IZR_NEG_POS.
-  - simpl. unfold IZR. rewrite <- 3!INR_IPR, Pos2Nat.inj_add, plus_INR.
-    ring.
-Qed.
-
-Lemma mult_IPR : forall n m:positive, IPR (n * m) == IPR n * IPR m.
-Proof.
-  intros. repeat rewrite <- INR_IPR.
-  rewrite Pos2Nat.inj_mul. apply mult_INR.
-Qed.
-
-(**********)
-Lemma mult_IZR : forall n m:Z, IZR (n * m) == IZR n * IZR m.
-Proof.
-  intros n m. destruct n.
-  - rewrite Rmult_0_l. rewrite Z.mul_0_l. reflexivity.
-  - destruct m. rewrite Z.mul_0_r, Rmult_0_r. reflexivity.
-    simpl; unfold IZR. apply mult_IPR.
-    simpl. unfold IZR. rewrite mult_IPR. ring.
-  - destruct m. rewrite Z.mul_0_r, Rmult_0_r. reflexivity.
-    simpl. unfold IZR. rewrite mult_IPR. ring.
-    simpl. unfold IZR. rewrite mult_IPR. ring.
-Qed.
-
-Lemma pow_IZR : forall z n, pow (IZR z) n == IZR (Z.pow z (Z.of_nat n)).
-Proof.
- intros z [|n];simpl; trivial. reflexivity.
- rewrite Zpower_pos_nat.
- rewrite SuccNat2Pos.id_succ. unfold Zpower_nat;simpl.
- rewrite mult_IZR.
- induction n;simpl;trivial. reflexivity.
- rewrite mult_IZR;ring[IHn].
-Qed.
-
-(**********)
-Lemma succ_IZR : forall n:Z, IZR (Z.succ n) == IZR n + 1.
-Proof.
-  intro; unfold Z.succ; apply plus_IZR.
-Qed.
-
-(**********)
-Lemma opp_IZR : forall n:Z, IZR (- n) == - IZR n.
-Proof.
-  intros [|z|z]; unfold IZR; simpl; auto with creal.
-  ring.
-  reflexivity. rewrite Ropp_involutive. reflexivity.
-Qed.
-
-Definition Ropp_Ropp_IZR := opp_IZR.
-
-Lemma minus_IZR : forall n m:Z, IZR (n - m) == IZR n - IZR m.
-Proof.
-  intros; unfold Z.sub, Rminus,CRminus.
-  rewrite <- opp_IZR.
-  apply plus_IZR.
-Qed.
-
-(**********)
-Lemma Z_R_minus : forall n m:Z, IZR n - IZR m == IZR (n - m).
-Proof.
-  intros z1 z2; unfold Rminus,CRminus; unfold Z.sub.
-  rewrite <- (Ropp_Ropp_IZR z2); symmetry; apply plus_IZR.
-Qed.
-
-(**********)
-Lemma lt_0_IZR : forall n:Z, 0 < IZR n -> (0 < n)%Z.
-Proof.
-  intro z; case z; simpl; intros.
-  elim (Rlt_irrefl _ H).
-  easy.
-  elim (Rlt_not_le _ _ H).
-  unfold IZR.
-  rewrite <- INR_IPR.
-  auto with creal.
-Qed.
-
-(**********)
-Lemma lt_IZR : forall n m:Z, IZR n < IZR m -> (n < m)%Z.
-Proof.
-  intros z1 z2 H; apply Z.lt_0_sub.
-  apply lt_0_IZR.
-  rewrite <- Z_R_minus.
-  exact (Rgt_minus (IZR z2) (IZR z1) H).
-Qed.
-
-(**********)
-Lemma eq_IZR_R0 : forall n:Z, IZR n == 0 -> n = 0%Z.
-Proof.
-  intro z; destruct z; simpl; intros; auto with zarith.
-  unfold IZR in H. rewrite <- INR_IPR in H.
-  apply (INR_eq _ 0) in H.
-  exfalso. pose proof (Pos2Nat.is_pos p).
-  rewrite H in H0. inversion H0.
-  unfold IZR in H. rewrite <- INR_IPR in H.
-  apply (Rplus_eq_compat_r (INR (Pos.to_nat p))) in H.
-  rewrite Rplus_opp_l, Rplus_0_l in H. symmetry in H.
-  apply (INR_eq _ 0) in H.
-  exfalso. pose proof (Pos2Nat.is_pos p).
-  rewrite H in H0. inversion H0.
-Qed.
-
-(**********)
-Lemma eq_IZR : forall n m:Z, IZR n == IZR m -> n = m.
-Proof.
-  intros z1 z2 H; generalize (Rminus_diag_eq (IZR z1) (IZR z2) H);
-    rewrite (Z_R_minus z1 z2); intro; generalize (eq_IZR_R0 (z1 - z2) H0);
-      intro; omega.
-Qed.
-
-Lemma IZR_lt : forall n m:Z, (n < m)%Z -> IZR n < IZR m.
-Proof.
- assert (forall n:Z, Z.lt 0 n -> 0 < IZR n) as posCase.
- { intros. destruct (IZN n). apply Z.lt_le_incl. apply H.
-   subst n. rewrite <- INR_IZR_INZ. apply (lt_INR 0).
-   apply Nat2Z.inj_lt. apply H. }
-  intros. apply (Rplus_lt_reg_r (-(IZR n))).
-  pose proof minus_IZR. unfold Rminus,CRminus in H0.
-  repeat rewrite <- H0. unfold Zminus.
-  rewrite Z.add_opp_diag_r. apply posCase.
-  rewrite (Z.add_lt_mono_l _ _ n). ring_simplify. apply H.
-Qed.
-
-(**********)
-Lemma not_0_IZR : forall n:Z, n <> 0%Z -> IZR n # 0.
-Proof.
-  intros. destruct n. exfalso. apply H. reflexivity.
-  right. apply (IZR_lt 0). reflexivity.
-  left. apply (IZR_lt _ 0). reflexivity.
-Qed.
-
-(*********)
-Lemma le_0_IZR : forall n:Z, 0 <= IZR n -> (0 <= n)%Z.
-Proof.
-  intros. destruct n. discriminate. discriminate.
-  exfalso. rewrite <- Ropp_0 in H. unfold IZR in H. apply H.
-  apply Ropp_gt_lt_contravar. rewrite <- INR_IPR.
-  apply (lt_INR 0). apply Pos2Nat.is_pos.
-Qed.
-
-(**********)
-Lemma le_IZR : forall n m:Z, IZR n <= IZR m -> (n <= m)%Z.
-Proof.
-  intros. apply (Rplus_le_compat_r (-(IZR n))) in H.
-  pose proof minus_IZR. unfold Rminus,CRminus in H0.
-  repeat rewrite <- H0 in H. unfold Zminus in H.
-  rewrite Z.add_opp_diag_r in H.
-  apply (Z.add_le_mono_l _ _ (-n)). ring_simplify.
-  rewrite Z.add_comm. apply le_0_IZR. apply H.
-Qed.
-
-(**********)
-Lemma le_IZR_R1 : forall n:Z, IZR n <= 1 -> (n <= 1)%Z.
-Proof.
-  intros. apply (le_IZR n 1). apply H.
-Qed.
-
-(**********)
-Lemma IZR_ge : forall n m:Z, (n >= m)%Z -> IZR n >= IZR m.
-Proof.
-  intros m n H; apply Rnot_lt_ge. intro abs.
-  apply lt_IZR in abs. omega.
-Qed.
-
-Lemma IZR_le : forall n m:Z, (n <= m)%Z -> IZR n <= IZR m.
-Proof.
-  intros m n H; apply Rnot_lt_ge. intro abs.
-  apply lt_IZR in abs. omega.
-Qed.
-
-Lemma IZR_neq : forall z1 z2:Z, z1 <> z2 -> IZR z1 # IZR z2.
-Proof.
-  intros. destruct (not_0_IZR (z1-z2)).
-  intro abs. apply H. rewrite <- (Z.add_cancel_r _ _ (-z2)).
-  ring_simplify. exact abs.
-  left. apply IZR_lt. apply (lt_IZR _ 0) in c.
-  rewrite (Z.add_lt_mono_r _ _ (-z2)).
-  ring_simplify. exact c.
-  right. apply IZR_lt. apply (lt_IZR 0) in c.
-  rewrite (Z.add_lt_mono_l _ _ (-z2)).
-  ring_simplify. rewrite Z.add_comm. exact c.
-Qed.
-
-Hint Extern 0 (IZR _ <= IZR _) => apply IZR_le, Zle_bool_imp_le, eq_refl : creal.
-Hint Extern 0 (IZR _ >= IZR _) => apply Rle_ge, IZR_le, Zle_bool_imp_le, eq_refl : creal.
-Hint Extern 0 (IZR _ <  IZR _) => apply IZR_lt, eq_refl : creal.
-Hint Extern 0 (IZR _ >  IZR _) => apply IZR_lt, eq_refl : creal.
-Hint Extern 0 (IZR _ <> IZR _) => apply IZR_neq, Zeq_bool_neq, eq_refl : creal.
-
-Lemma one_IZR_lt1 : forall n:Z, -(1) < IZR n < 1 -> n = 0%Z.
-Proof.
-  intros z [H1 H2].
-  apply Z.le_antisymm.
-  apply Z.lt_succ_r; apply lt_IZR; trivial.
-  change 0%Z with (Z.succ (-1)).
-  apply Z.le_succ_l; apply lt_IZR; trivial.
-Qed.
-
-Lemma one_IZR_r_R1 :
-  forall r (n m:Z), r < IZR n <= r + 1 -> r < IZR m <= r + 1 -> n = m.
-Proof.
-  intros r z x [H1 H2] [H3 H4].
-  cut ((z - x)%Z = 0%Z); auto with zarith.
-  apply one_IZR_lt1.
-  split; rewrite <- Z_R_minus.
-  setoid_replace (-(1)) with (r - (r + 1)).
-  unfold CReal_minus; apply Rplus_lt_le_compat; auto with creal.
-  ring.
-  setoid_replace 1 with (r + 1 - r).
-  unfold CReal_minus; apply Rplus_le_lt_compat; auto with creal.
-  ring.
-Qed.
-
-
-(**********)
-Lemma single_z_r_R1 :
-  forall r (n m:Z),
-    r < IZR n -> IZR n <= r + 1 -> r < IZR m -> IZR m <= r + 1 -> n = m.
-Proof.
-  intros; apply one_IZR_r_R1 with r; auto.
-Qed.
-
-(**********)
-Lemma tech_single_z_r_R1 :
-  forall r (n:Z),
-    r < IZR n ->
-    IZR n <= r + 1 ->
-    { s : Z & prod (s <> n) (r < IZR s <= r + 1) } -> False.
-Proof.
-  intros r z H1 H2 [s [H3 [H4 H5]]].
-  apply H3; apply single_z_r_R1 with r; trivial.
-Qed.
-
-
-Lemma Rmult_le_compat_l_half : forall r r1 r2,
-    0 < r -> r1 <= r2 -> r * r1 <= r * r2.
-Proof.
-  intros. intro abs. apply (Rmult_lt_reg_l) in abs.
-  contradiction. apply H.
-Qed.
-
-Lemma INR_CR_of_Q : forall (n : nat),
-    CR_of_Q CR (Z.of_nat n # 1) == INR n.
-Proof.
-  induction n.
-  - apply CR_of_Q_zero.
-  - transitivity (CR_of_Q CR (1 + (Z.of_nat n # 1))).
-    replace (S n) with (1 + n)%nat. 2: reflexivity.
-    rewrite (Nat2Z.inj_add 1 n).
-    apply CR_of_Q_proper.
-    rewrite <- (Qinv_plus_distr (Z.of_nat 1) (Z.of_nat n) 1). reflexivity.
-    rewrite CR_of_Q_plus. rewrite IHn. clear IHn.
-    setoid_replace (INR (S n)) with (1 + INR n).
-    rewrite CR_of_Q_one. reflexivity.
-    simpl. destruct n. rewrite Rplus_0_r. reflexivity.
-    rewrite Rplus_comm. reflexivity.
-Qed.
-
-Definition Rup_nat (x : R)
-  : { n : nat & x < INR n }.
-Proof.
-  intros. destruct (CR_archimedean CR x) as [p maj].
-  exists (Pos.to_nat p).
-  rewrite <- INR_CR_of_Q, positive_nat_Z. exact maj.
-Qed.
-
-Fixpoint Rarchimedean_ind (x:R) (n : Z) (p:nat) { struct p }
-  : (x < IZR n < x + 2 + (INR p))
-    -> { n:Z & x < IZR n < x+2 }.
-Proof.
-  destruct p.
-  - exists n. destruct H. split. exact r. rewrite Rplus_0_r in r0; exact r0.
-  - intros. destruct (linear_order_T (x+1+INR p) (IZR n) (x+2+INR p)).
-    do 2 rewrite Rplus_assoc. apply Rplus_lt_compat_l, Rplus_lt_compat_r.
-    rewrite <- (Rplus_0_r 1). apply Rplus_lt_compat_l. apply Rlt_0_1.
-    + apply (Rarchimedean_ind x (n-1)%Z p). unfold Zminus.
-      split; rewrite plus_IZR, opp_IZR.
-      setoid_replace (IZR 1) with 1. 2: reflexivity.
-      apply (Rplus_lt_reg_l 1). ring_simplify.
-      apply (Rle_lt_trans _ (x + 1 + INR p)). 2: exact r.
-      rewrite Rplus_assoc. apply Rplus_le_compat_l.
-      rewrite <- (Rplus_0_r 1), Rplus_assoc. apply Rplus_le_compat_l.
-      rewrite Rplus_0_l. apply (le_INR 0), le_0_n.
-      setoid_replace (IZR 1) with 1. 2: reflexivity.
-      apply (Rplus_lt_reg_l 1). ring_simplify.
-      setoid_replace (x + 2 + INR p + 1) with (x + 2 + INR (S p)).
-      apply H. rewrite S_INR. ring.
-    + apply (Rarchimedean_ind x n p). split. apply H. exact r.
-Qed.
-
-Lemma Rarchimedean (x:R) : { n : Z & x < IZR n < x + 2 }.
-Proof.
-  destruct (Rup_nat x) as [n nmaj].
-  destruct (Rup_nat (INR n + - (x + 2))) as [p pmaj].
-  apply (Rplus_lt_compat_r (x+2)) in pmaj.
-  rewrite Rplus_assoc, Rplus_opp_l, Rplus_0_r in pmaj.
-  apply (Rarchimedean_ind x (Z.of_nat n) p).
-  split; rewrite <- INR_IZR_INZ. exact nmaj.
-  rewrite Rplus_comm in pmaj. exact pmaj.
-Qed.
-
-Lemma Rmult_le_0_compat : forall a b,
-    0 <= a -> 0 <= b -> 0 <= a * b.
-Proof.
-  (* Limit of (a + 1/n)*b when n -> infty. *)
-  intros. intro abs.
-  assert (0 < -(a*b)) as epsPos.
-  { rewrite <- Ropp_0. apply Ropp_gt_lt_contravar. apply abs. }
-  pose proof (Rup_nat (b * (/ (-(a*b))) (inr (Ropp_0_gt_lt_contravar _ abs))))
-    as [n maj].
-  destruct n as [|n].
-  - simpl in maj. apply (Rmult_lt_compat_r (-(a*b))) in maj.
-    rewrite Rmult_0_l in maj.
-    rewrite Rmult_assoc in maj. rewrite Rinv_l in maj.
-    rewrite Rmult_1_r in maj. contradiction.
-    apply epsPos.
-  - (* n > 0 *)
-    assert (0 < INR (S n)) as nPos.
-    { apply (lt_INR 0). apply le_n_S, le_0_n. }
-    assert (b * (/ (INR (S n))) (inr nPos) < -(a*b)).
-    { apply (Rmult_lt_reg_r (INR (S n))). apply nPos.
-      rewrite Rmult_assoc. rewrite Rinv_l.
-      rewrite Rmult_1_r. apply (Rmult_lt_compat_r (-(a*b))) in maj.
-      rewrite Rmult_assoc in maj. rewrite Rinv_l in maj.
-      rewrite Rmult_1_r in maj. rewrite Rmult_comm.
-      apply maj. exact epsPos. }
-    pose proof (Rmult_le_compat_l_half (a + (/ (INR (S n))) (inr nPos))
-                                       0 b).
-    assert (a + (/ (INR (S n))) (inr nPos) > 0 + 0).
-    apply Rplus_le_lt_compat. apply H. apply Rinv_0_lt_compat.
-    rewrite Rplus_0_l in H3. specialize (H2 H3 H0).
-    clear H3. rewrite Rmult_0_r in H2.
-    apply H2. clear H2. rewrite Rmult_plus_distr_r.
-    apply (Rplus_lt_compat_l (a*b)) in H1.
-    rewrite Rplus_opp_r in H1.
-    rewrite (Rmult_comm ((/ (INR (S n))) (inr nPos))).
-    apply H1.
-Qed.
-
-Lemma Rmult_le_compat_l : forall r r1 r2,
-    0 <= r -> r1 <= r2 -> r * r1 <= r * r2.
-Proof.
-  intros. apply Rminus_ge. apply Rge_minus in H0.
-  unfold Rminus,CRminus. rewrite Ropp_mult_distr_r.
-  rewrite <- Rmult_plus_distr_l.
-  apply Rmult_le_0_compat; assumption.
-Qed.
-Hint Resolve Rmult_le_compat_l: creal.
-
-Lemma Rmult_le_compat_r : forall r r1 r2,
-    0 <= r -> r1 <= r2 -> r1 * r <= r2 * r.
-Proof.
-  intros. rewrite <- (Rmult_comm r). rewrite <- (Rmult_comm r).
-  apply Rmult_le_compat_l; assumption.
-Qed.
-Hint Resolve Rmult_le_compat_r: creal.
-
-(*********)
-Lemma Rmult_le_0_lt_compat :
-  forall r1 r2 r3 r4,
-    0 <= r1 -> 0 <= r3 -> r1 < r2 -> r3 < r4 -> r1 * r3 < r2 * r4.
-Proof.
-  intros. apply (Rle_lt_trans _ (r2 * r3)).
-  apply Rmult_le_compat_r. apply H0. intro abs. apply (Rlt_asym r1 r2 H1).
-  apply abs. apply Rmult_lt_compat_l. exact (Rle_lt_trans 0 r1 r2 H H1).
-  exact H2.
-Qed.
-
-Lemma Rmult_le_compat_neg_l :
-  forall r r1 r2, r <= 0 -> r1 <= r2 -> r * r2 <= r * r1.
-Proof.
-  intros. apply Ropp_le_cancel.
-  do 2 rewrite Ropp_mult_distr_l. apply Rmult_le_compat_l.
-  2: exact H0. apply Ropp_0_ge_le_contravar. exact H.
-Qed.
-Hint Resolve Rmult_le_compat_neg_l: creal.
-
-Lemma Rmult_le_ge_compat_neg_l :
-  forall r r1 r2, r <= 0 -> r1 <= r2 -> r * r1 >= r * r2.
-Proof.
-  intros; apply Rle_ge; auto with creal.
-Qed.
-Hint Resolve Rmult_le_ge_compat_neg_l: creal.
-
-
-(**********)
-Lemma Rmult_ge_compat_l :
-  forall r r1 r2, r >= 0 -> r1 >= r2 -> r * r1 >= r * r2.
-Proof.
-  intros. apply Rmult_le_compat_l; assumption.
-Qed.
-
-Lemma Rmult_ge_compat_r :
-  forall r r1 r2, r >= 0 -> r1 >= r2 -> r1 * r >= r2 * r.
-Proof.
-  intros. apply Rmult_le_compat_r; assumption.
-Qed.
-
-
-(**********)
-Lemma Rmult_le_compat :
-  forall r1 r2 r3 r4,
-    0 <= r1 -> 0 <= r3 -> r1 <= r2 -> r3 <= r4 -> r1 * r3 <= r2 * r4.
-Proof.
-  intros x y z t H' H'0 H'1 H'2.
-  apply Rle_trans with (r2 := x * t); auto with creal.
-  repeat rewrite (fun x => Rmult_comm x t).
-  apply Rmult_le_compat_l; auto.
-  apply Rle_trans with z; auto.
-Qed.
-Hint Resolve Rmult_le_compat: creal.
-
-Lemma Rmult_ge_compat :
-  forall r1 r2 r3 r4,
-    r2 >= 0 -> r4 >= 0 -> r1 >= r2 -> r3 >= r4 -> r1 * r3 >= r2 * r4.
-Proof. auto with creal rorders. Qed.
-
-Lemma mult_IPR_IZR : forall (n:positive) (m:Z), IZR (Z.pos n * m) == IPR n * IZR m.
-Proof.
-  intros. rewrite mult_IZR. apply Rmult_eq_compat_r. reflexivity.
-Qed.
-
-Definition IQR (q:Q) : R :=
-  match q with
-  | Qmake a b => IZR a * (/ (IPR b)) (inr (IPR_pos b))
-  end.
-Arguments IQR q%Q : simpl never.
-
-Lemma plus_IQR : forall n m:Q, IQR (n + m) == IQR n + IQR m.
-Proof.
-  intros. destruct n,m; unfold Qplus,IQR; simpl.
-  rewrite plus_IZR. repeat rewrite mult_IZR.
-  setoid_replace ((/ IPR (Qden * Qden0)) (inr (IPR_pos (Qden * Qden0))))
-    with ((/ IPR Qden) (inr (IPR_pos Qden))
-          * (/ IPR Qden0) (inr (IPR_pos Qden0))).
-  rewrite Rmult_plus_distr_r.
-  repeat rewrite Rmult_assoc. rewrite <- (Rmult_assoc (IZR (Z.pos Qden))).
-  rewrite Rinv_r. rewrite Rmult_1_l.
-  rewrite (Rmult_comm ((/IPR Qden) (inr (IPR_pos Qden)))).
-  rewrite <- (Rmult_assoc (IZR (Z.pos Qden0))).
-  rewrite Rinv_r. rewrite Rmult_1_l. reflexivity. unfold IZR.
-  right. apply IPR_pos.
-  right. apply IPR_pos.
-  rewrite <- (Rinv_mult_distr
-                _ _ _ _ (inr (Rmult_lt_0_compat _ _ (IPR_pos _) (IPR_pos _)))).
-  apply Rinv_eq_compat. apply mult_IPR.
-Qed.
-
-Lemma IQR_pos : forall q:Q, Qlt 0 q -> 0 < IQR q.
-Proof.
-  intros. destruct q; unfold IQR.
-  apply Rmult_lt_0_compat. apply (IZR_lt 0).
-  unfold Qlt in H; simpl in H.
-  rewrite Z.mul_1_r in H. apply H.
-  apply Rinv_0_lt_compat.
-Qed.
-
-Lemma opp_IQR : forall q:Q, IQR (- q) == - IQR q.
-Proof.
-  intros [a b]; unfold IQR; simpl.
-  rewrite Ropp_mult_distr_l.
-  rewrite opp_IZR. reflexivity.
-Qed.
-
-Lemma lt_IQR : forall n m:Q, IQR n < IQR m -> (n < m)%Q.
-Proof.
-  intros. destruct n,m; unfold IQR in H.
-  unfold Qlt; simpl. apply (Rmult_lt_compat_r (IPR Qden)) in H.
-  rewrite Rmult_assoc in H. rewrite Rinv_l in H.
-  rewrite Rmult_1_r in H. rewrite (Rmult_comm (IZR Qnum0)) in H.
-  apply (Rmult_lt_compat_l (IPR Qden0)) in H.
-  do 2 rewrite <- Rmult_assoc in H. rewrite Rinv_r in H.
-  rewrite Rmult_1_l in H.
-  rewrite (Rmult_comm (IZR Qnum0)) in H.
-  do 2 rewrite <- mult_IPR_IZR in H. apply lt_IZR in H.
-  rewrite Z.mul_comm. rewrite (Z.mul_comm Qnum0).
-  apply H.
-  right. rewrite <- INR_IPR. apply (lt_INR 0). apply Pos2Nat.is_pos.
-  rewrite <- INR_IPR. apply (lt_INR 0). apply Pos2Nat.is_pos.
-  apply IPR_pos.
-Qed.
-
-Lemma IQR_lt : forall n m:Q, Qlt n m -> IQR n < IQR m.
-Proof.
-  intros. apply (Rplus_lt_reg_r (-IQR n)).
-  rewrite Rplus_opp_r. rewrite <- opp_IQR. rewrite <- plus_IQR.
-  apply IQR_pos. apply (Qplus_lt_l _ _ n).
-  ring_simplify. apply H.
-Qed.
-
-Lemma IQR_nonneg : forall q:Q, Qle 0 q -> 0 <= (IQR q).
-Proof.
-  intros [a b] H. unfold IQR;simpl.
-  apply (Rle_trans _ (IZR a * 0)). rewrite Rmult_0_r. apply Rle_refl.
-  apply Rmult_le_compat_l.
-  apply (IZR_le 0 a). unfold Qle in H; simpl in H.
-  rewrite Z.mul_1_r in H. apply H.
-  unfold Rle. apply Rlt_asym. apply Rinv_0_lt_compat.
-Qed.
-
-Lemma IQR_le : forall n m:Q, Qle n m -> IQR n <= IQR m.
-Proof.
-  intros. apply (Rplus_le_reg_r (-IQR n)).
-  rewrite Rplus_opp_r. rewrite <- opp_IQR. rewrite <- plus_IQR.
-  apply IQR_nonneg. apply (Qplus_le_l _ _ n).
-  ring_simplify. apply H.
-Qed.
-
-Add Parametric Morphism : IQR
-    with signature Qeq ==> Req
-      as IQR_morph.
-Proof.
-  intros. destruct x,y; unfold IQR; simpl.
-  unfold Qeq in H; simpl in H.
-  apply (Rmult_eq_reg_r (IZR (Z.pos Qden))).
-  rewrite Rmult_assoc. rewrite Rinv_l. rewrite Rmult_1_r.
-  rewrite (Rmult_comm (IZR Qnum0)).
-  apply (Rmult_eq_reg_l (IZR (Z.pos Qden0))).
-  rewrite <- Rmult_assoc. rewrite <- Rmult_assoc. rewrite Rinv_r.
-  rewrite Rmult_1_l.
-  repeat rewrite <- mult_IZR.
-  rewrite <- H. rewrite Zmult_comm. reflexivity.
-  right. apply IPR_pos.
-  right. apply (IZR_lt 0). apply Pos2Z.is_pos.
-  right. apply IPR_pos.
-Qed.
-
-Instance IQR_morph_T
-  : CMorphisms.Proper
-      (CMorphisms.respectful Qeq Req) IQR.
-Proof.
-  intros x y H. destruct x,y; unfold IQR.
-  unfold Qeq in H; simpl in H.
-  apply (Rmult_eq_reg_r (IZR (Z.pos Qden))).
-  2: right; apply IPR_pos.
-  rewrite Rmult_assoc, Rinv_l, Rmult_1_r.
-  rewrite (Rmult_comm (IZR Qnum0)).
-  apply (Rmult_eq_reg_l (IZR (Z.pos Qden0))).
-  2: right; apply IPR_pos.
-  rewrite <- Rmult_assoc, <- Rmult_assoc, Rinv_r.
-  rewrite Rmult_1_l.
-  repeat rewrite <- mult_IZR.
-  rewrite <- H. rewrite Zmult_comm. reflexivity.
-  right; apply IPR_pos.
-Qed.
-
-Fixpoint Rfloor_pos (a : R) (n : nat) { struct n }
-  : 0 < a
-    -> a < INR n
-    -> { p : nat & INR p < a < INR p + 2 }.
-Proof.
-  (* Decreasing loop on n, until it is the first integer above a. *)
-  intros H H0. destruct n.
-  - exfalso. apply (Rlt_asym 0 a); assumption.
-  - destruct n as [|p] eqn:des.
-    + (* n = 1 *) exists O. split.
-      apply H. rewrite Rplus_0_l. apply (Rlt_trans a (1+0)).
-      rewrite Rplus_comm, Rplus_0_l. apply H0.
-      apply Rplus_le_lt_compat.
-      apply Rle_refl. apply Rlt_0_1.
-    + (* n > 1 *)
-      destruct (linear_order_T (INR p) a (INR (S p))).
-      * rewrite <- Rplus_0_l, S_INR, Rplus_comm. apply Rplus_lt_compat_l.
-        apply Rlt_0_1.
-      * exists p. split. exact r.
-        rewrite S_INR, S_INR, Rplus_assoc in H0. exact H0.
-      * apply (Rfloor_pos a n H). rewrite des. apply r.
-Qed.
-
-Definition Rfloor (a : R)
-  : { p : Z & IZR p < a < IZR p + 2 }.
-Proof.
-  destruct (linear_order_T 0 a 1 Rlt_0_1).
-  - destruct (Rup_nat a). destruct (Rfloor_pos a x r r0).
-    exists (Z.of_nat x0). split; rewrite <- INR_IZR_INZ; apply p.
-  - apply (Rplus_lt_compat_l (-a)) in r.
-    rewrite Rplus_comm, Rplus_opp_r, Rplus_comm in r.
-    destruct (Rup_nat (1-a)).
-    destruct (Rfloor_pos (1-a) x r r0).
-    exists (-(Z.of_nat x0 + 1))%Z. split; rewrite opp_IZR, plus_IZR.
-    + rewrite <- (Ropp_involutive a). apply Ropp_gt_lt_contravar.
-      destruct p as [_ a0]. apply (Rplus_lt_reg_r 1).
-      rewrite Rplus_comm, Rplus_assoc. rewrite <- INR_IZR_INZ. apply a0.
-    + destruct p as [a0 _]. apply (Rplus_lt_compat_l a) in a0.
-      unfold Rminus in a0.
-      rewrite <- (Rplus_comm (1+-a)), Rplus_assoc, Rplus_opp_l, Rplus_0_r in a0.
-      rewrite <- INR_IZR_INZ.
-      apply (Rplus_lt_reg_r (INR x0)). unfold IZR, IPR, IPR_2.
-      ring_simplify. exact a0.
-Qed.
-
-(* A point in an archimedean field is the limit of a
-   sequence of rational numbers (n maps to the q between
-   a and a+1/n). This is how real numbers compute,
-   and they are measured by exact rational numbers. *)
-Definition RQ_dense (a b : R)
-  : a < b -> { q : Q & a < IQR q < b }.
-Proof.
-  intros H0.
-  assert (0 < b - a) as epsPos.
-  { apply (Rplus_lt_compat_r (-a)) in H0.
-    rewrite Rplus_opp_r in H0. apply H0. }
-  pose proof (Rup_nat ((/(b-a)) (inr epsPos)))
-    as [n maj].
-  destruct n as [|k].
-  - exfalso.
-    apply (Rmult_lt_compat_l (b-a)) in maj. 2: apply epsPos.
-    rewrite Rmult_0_r in maj. rewrite Rinv_r in maj.
-    apply (Rlt_asym 0 1). apply Rlt_0_1. apply maj.
-    right. apply epsPos.
-  - (* 0 < n *)
-    pose (Pos.of_nat (S k)) as n.
-    destruct (Rfloor (IZR (2 * Z.pos n) * b)) as [p maj2].
-    exists (p # (2*n))%Q. split.
-    + apply (Rlt_trans a (b - IQR (1 # n))).
-      apply (Rplus_lt_reg_r (IQR (1#n))).
-      unfold Rminus,CRminus. rewrite Rplus_assoc. rewrite Rplus_opp_l.
-      rewrite Rplus_0_r. apply (Rplus_lt_reg_l (-a)).
-      rewrite <- Rplus_assoc, Rplus_opp_l, Rplus_0_l.
-      rewrite Rplus_comm. unfold IQR.
-      rewrite Rmult_1_l. apply (Rmult_lt_reg_l (IPR n)).
-      apply IPR_pos. rewrite Rinv_r.
-      apply (Rmult_lt_compat_l (b-a)) in maj.
-      rewrite Rinv_r, Rmult_comm in maj.
-      rewrite <- INR_IPR. unfold n. rewrite Nat2Pos.id.
-      apply maj. discriminate. right. exact epsPos. exact epsPos.
-      right. apply IPR_pos.
-      apply (Rplus_lt_reg_r (IQR (1 # n))).
-      unfold Rminus,CRminus. rewrite Rplus_assoc, Rplus_opp_l.
-      rewrite Rplus_0_r. rewrite <- plus_IQR.
-      destruct maj2 as [_ maj2].
-      setoid_replace ((p # 2 * n) + (1 # n))%Q
-        with ((p + 2 # 2 * n))%Q. unfold IQR.
-      apply (Rmult_lt_reg_r (IZR (Z.pos (2 * n)))).
-      apply (IZR_lt 0). reflexivity. rewrite Rmult_assoc.
-      rewrite Rinv_l. rewrite Rmult_1_r. rewrite Rmult_comm.
-      rewrite plus_IZR. apply maj2.
-      setoid_replace (1#n)%Q with (2#2*n)%Q. 2: reflexivity.
-      apply Qinv_plus_distr.
-    + destruct maj2 as [maj2 _]. unfold IQR.
-      apply (Rmult_lt_reg_r (IZR (Z.pos (2 * n)))).
-      apply (IZR_lt 0). apply Pos2Z.is_pos. rewrite Rmult_assoc, Rinv_l.
-      rewrite Rmult_1_r, Rmult_comm. apply maj2.
-Qed.
-
-Definition RQ_limit : forall (x : R) (n:nat),
-    { q:Q & x < IQR q < x + IQR (1 # Pos.of_nat n) }.
-Proof.
-  intros x n. apply (RQ_dense x (x + IQR (1 # Pos.of_nat n))).
-  rewrite <- (Rplus_0_r x). rewrite Rplus_assoc.
-  apply Rplus_lt_compat_l. rewrite Rplus_0_l. apply IQR_pos.
-  reflexivity.
-Qed.
-
-(* Rlt is decided by the LPO in Type,
-   which is a non-constructive oracle. *)
-Lemma Rlt_lpo_dec : forall x y : R,
-    (forall (P : nat -> Prop), (forall n, {P n} + {~P n})
-                    -> {n | ~P n} + {forall n, P n})
-    -> (x < y) + (y <= x).
-Proof.
-  intros x y lpo.
-  pose (fun n => let (l,_) := RQ_limit x n in l) as xn.
-  pose (fun n => let (l,_) := RQ_limit y n in l) as yn.
-  destruct (lpo (fun n:nat => Qle (yn n - xn n) (1 # Pos.of_nat n))).
-  - intro n. destruct (Qlt_le_dec (1 # Pos.of_nat n) (yn n - xn n)).
-    right. apply Qlt_not_le. exact q. left. exact q.
-  - left. destruct s as [n nmaj]. unfold xn,yn in nmaj.
-    destruct (RQ_limit x n), (RQ_limit y n); unfold proj1_sig in nmaj.
-    apply Qnot_le_lt in nmaj.
-    apply (Rlt_le_trans x (IQR x0)). apply p.
-    apply (Rle_trans _ (IQR (x1 - (1# Pos.of_nat n)))).
-    apply IQR_le. apply (Qplus_le_l _ _ ((1#Pos.of_nat n) - x0)).
-    ring_simplify. ring_simplify in nmaj. rewrite Qplus_comm.
-    apply Qlt_le_weak. exact nmaj.
-    unfold Qminus. rewrite plus_IQR,opp_IQR.
-    apply (Rplus_le_reg_r (IQR (1#Pos.of_nat n))).
-    ring_simplify. unfold Rle. apply Rlt_asym. rewrite Rplus_comm. apply p0.
-  - right. intro abs.
-    pose ((y - x) * IQR (1#2)) as eps.
-    assert (0 < eps) as epsPos.
-    { apply Rmult_lt_0_compat. apply Rgt_minus. exact abs.
-      apply IQR_pos. reflexivity. }
-    destruct (Rup_nat ((/eps) (inr epsPos))) as [n nmaj].
-    specialize (q (S n)). unfold xn, yn in q.
-    destruct (RQ_limit x (S n)) as [a amaj], (RQ_limit y (S n)) as [b bmaj];
-      unfold proj1_sig in q.
-    assert (IQR (1 # Pos.of_nat (S n)) < eps).
-    { unfold IQR. rewrite Rmult_1_l.
-      apply (Rmult_lt_reg_l (IPR (Pos.of_nat (S n)))). apply IPR_pos.
-      rewrite Rinv_r, <- INR_IPR, Nat2Pos.id. 2: discriminate.
-      apply (Rlt_trans _ _ (INR (S n))) in nmaj.
-      apply (Rmult_lt_compat_l eps) in nmaj.
-      rewrite Rinv_r, Rmult_comm in nmaj. exact nmaj.
-      right. exact epsPos. exact epsPos. apply lt_INR. apply le_n_S, le_refl.
-      right. apply IPR_pos. }
-    unfold eps in H. apply (Rlt_asym y (IQR b)).
-    + apply bmaj.
-    + apply (Rlt_le_trans _ (IQR a + (y - x) * IQR (1 # 2))).
-      apply IQR_le in q.
-      apply (Rle_lt_trans _ _ _ q) in H.
-      apply (Rplus_lt_reg_l (-IQR a)).
-      rewrite <- Rplus_assoc, Rplus_opp_l, Rplus_0_l, Rplus_comm,
-      <- opp_IQR, <- plus_IQR. exact H.
-      apply (Rplus_lt_compat_l x) in H.
-      destruct amaj. apply (Rlt_trans _ _ _ r0) in H.
-      apply (Rplus_lt_compat_r ((y - x) * IQR (1 # 2))) in H.
-      unfold Rle. apply Rlt_asym.
-      setoid_replace (x + (y - x) * IQR (1 # 2) + (y - x) * IQR (1 # 2)) with y in H.
-      exact H.
-      rewrite Rplus_assoc, <- Rmult_plus_distr_r.
-      setoid_replace (y - x + (y - x)) with ((y-x)*2).
-      unfold IQR. rewrite Rmult_1_l, Rmult_assoc, Rinv_r. ring.
-      right. apply (IZR_lt 0). reflexivity.
-      unfold IZR, IPR, IPR_2. ring.
-Qed.
-
-Lemma Rlt_lpo_floor : forall x : R,
-    (forall (P : nat -> Prop), (forall n, {P n} + {~P n})
-                    -> {n | ~P n} + {forall n, P n})
-    -> { p : Z & IZR p <= x < IZR p + 1 }.
-Proof.
-  intros x lpo. destruct (Rfloor x) as [n [H H0]].
-  destruct (Rlt_lpo_dec x (IZR n + 1) lpo).
-  - exists n. split. unfold Rle. apply Rlt_asym. exact H. exact r.
-  - exists (n+1)%Z. split. rewrite plus_IZR. exact r.
-    rewrite plus_IZR, Rplus_assoc. exact H0.
-Qed.
-
-
-(*********)
-Lemma Rmult_le_pos : forall r1 r2, 0 <= r1 -> 0 <= r2 -> 0 <= r1 * r2.
-Proof.
-  intros x y H H0; rewrite <- (Rmult_0_l x); rewrite <- (Rmult_comm x);
-    apply (Rmult_le_compat_l x 0 y H H0).
-Qed.
-
-Lemma Rinv_le_contravar :
-  forall x y (xpos : 0 < x) (ynz : y # 0),
-    x <= y -> (/ y) ynz <= (/ x) (inr xpos).
-Proof.
-  intros. intro abs. apply (Rmult_lt_compat_l x) in abs.
-  2: apply xpos. rewrite Rinv_r in abs.
-  apply (Rmult_lt_compat_r y) in abs.
-  rewrite Rmult_assoc in abs. rewrite Rinv_l in abs.
-  rewrite Rmult_1_r in abs. rewrite Rmult_1_l in abs. contradiction.
-  exact (Rlt_le_trans _ x _ xpos H).
-  right. exact xpos.
-Qed.
-
-Lemma Rle_Rinv : forall x y (xpos : 0 < x) (ypos : 0 < y),
-    x <= y -> (/ y) (inr ypos) <= (/ x) (inr xpos).
-Proof.
-  intros.
-  apply Rinv_le_contravar with (1 := H).
-Qed.
-
-Lemma Ropp_div : forall x y (ynz : y # 0),
-    -x * (/y) ynz == - (x * (/ y) ynz).
-Proof.
-  intros; ring.
-Qed.
-
-Lemma double : forall r1, 2 * r1 == r1 + r1.
-Proof.
-  intros. rewrite (Rmult_plus_distr_r 1 1 r1), Rmult_1_l. reflexivity.
-Qed.
-
-Lemma Rlt_0_2 : 0 < 2.
-Proof.
-  apply (Rlt_trans 0 (0+1)). rewrite Rplus_0_l. exact Rlt_0_1.
-  apply Rplus_lt_le_compat. exact Rlt_0_1. apply Rle_refl.
-Qed.
-
-Lemma double_var : forall r1, r1 == r1 * (/ 2) (inr Rlt_0_2)
-                                    + r1 * (/ 2) (inr Rlt_0_2).
-Proof.
-  intro; rewrite <- double; rewrite <- Rmult_assoc;
-    symmetry ; apply Rinv_r_simpl_m.
-Qed.
-
-(* IZR : Z -> R is a ring morphism *)
-Lemma R_rm : ring_morph
-  0 1 Rplus Rmult Rminus Ropp Req
-  0%Z 1%Z Zplus Zmult Zminus Z.opp Zeq_bool IZR.
-Proof.
-constructor ; try easy.
-exact plus_IZR.
-exact minus_IZR.
-exact mult_IZR.
-exact opp_IZR.
-intros x y H.
-replace y with x. reflexivity.
-now apply Zeq_bool_eq.
-Qed.
-
-Lemma Zeq_bool_IZR x y :
-  IZR x == IZR y -> Zeq_bool x y = true.
-Proof.
-intros H.
-apply Zeq_is_eq_bool.
-now apply eq_IZR.
-Qed.
-
-
-(*********************************************************)
-(** ** Other rules about < and <=                        *)
-(*********************************************************)
-
-Lemma Rmult_ge_0_gt_0_lt_compat :
-  forall r1 r2 r3 r4,
-    r3 >= 0 -> r2 > 0 -> r1 < r2 -> r3 < r4 -> r1 * r3 < r2 * r4.
-Proof.
-  intros. apply (Rle_lt_trans _ (r2 * r3)).
-  apply Rmult_le_compat_r. apply H. unfold Rle. apply Rlt_asym. apply H1.
-  apply Rmult_lt_compat_l. apply H0. apply H2.
-Qed.
-
-Lemma le_epsilon :
-  forall r1 r2, (forall eps, 0 < eps -> r1 <= r2 + eps) -> r1 <= r2.
-Proof.
-  intros x y H. intro abs.
-  assert (0 < (x - y) * (/ 2) (inr Rlt_0_2)).
-  { apply (Rplus_lt_compat_r (-y)) in abs. rewrite Rplus_opp_r in abs.
-    apply Rmult_lt_0_compat. exact abs.
-    apply Rinv_0_lt_compat. }
-  specialize (H ((x - y) * (/ 2) (inr Rlt_0_2)) H0).
-  apply (Rmult_le_compat_l 2) in H.
-  rewrite Rmult_plus_distr_l in H.
-  apply (Rplus_le_compat_l (-x)) in H.
-  rewrite (Rmult_comm (x-y)), <- Rmult_assoc, Rinv_r, Rmult_1_l,
-  (Rmult_plus_distr_r 1 1), (Rmult_plus_distr_r 1 1)
-    in H.
-  ring_simplify in H; contradiction.
-  right. apply Rlt_0_2. unfold Rle. apply Rlt_asym. apply Rlt_0_2.
-Qed.
-
-(**********)
-Lemma Rdiv_lt_0_compat : forall a b (bpos : 0 < b),
-    0 < a -> 0 < a * (/b) (inr bpos).
-Proof.
-intros; apply Rmult_lt_0_compat;[|apply Rinv_0_lt_compat]; assumption.
-Qed.
-
-Lemma Rdiv_plus_distr : forall a b c (cnz : c # 0),
-    (a + b)* (/c) cnz == a* (/c) cnz + b* (/c) cnz.
-Proof.
-  intros. apply Rmult_plus_distr_r.
-Qed.
-
-Lemma Rdiv_minus_distr : forall a b c (cnz : c # 0),
-    (a - b)* (/c) cnz == a* (/c) cnz - b* (/c) cnz.
-Proof.
-  intros; unfold Rminus,CRminus; rewrite Rmult_plus_distr_r.
-  apply Rplus_morph. reflexivity.
-  rewrite Ropp_mult_distr_l. reflexivity.
-Qed.
-
-
-(*********************************************************)
-(** * Definitions of new types                           *)
-(*********************************************************)
-
-Record nonnegreal : Type := mknonnegreal
-  {nonneg :> R; cond_nonneg : 0 <= nonneg}.
-
-Record posreal : Type := mkposreal {pos :> R; cond_pos : 0 < pos}.
-
-Record nonposreal : Type := mknonposreal
-  {nonpos :> R; cond_nonpos : nonpos <= 0}.
-
-Record negreal : Type := mknegreal {neg :> R; cond_neg : neg < 0}.
-
-Record nonzeroreal : Type := mknonzeroreal
-  {nonzero :> R; cond_nonzero : nonzero <> 0}.
diff --git a/theories/Reals/ConstructiveRcomplete.v b/theories/Reals/ConstructiveRcomplete.v
index 0a515672f2..b575c17961 100644
--- a/theories/Reals/ConstructiveRcomplete.v
+++ b/theories/Reals/ConstructiveRcomplete.v
@@ -11,6 +11,7 @@
 
 Require Import QArith_base.
 Require Import Qabs.
+Require Import ConstructiveReals.
 Require Import ConstructiveCauchyRealsMult.
 Require Import Logic.ConstructiveEpsilon.
 
@@ -347,3 +348,35 @@ Proof.
       apply Qplus_le_r. discriminate.
       rewrite Qinv_plus_distr. reflexivity.
 Qed.
+
+Definition CRealImplem : ConstructiveReals.
+Proof.
+  assert (isLinearOrder CReal CRealLt) as lin.
+  { repeat split. exact CRealLt_asym.
+    exact CReal_lt_trans.
+    intros. destruct (CRealLt_dec x z y H).
+    left. exact c. right. exact c. }
+  apply (Build_ConstructiveReals
+           CReal CRealLt lin CRealLtProp
+           CRealLtEpsilon CRealLtForget CRealLtDisjunctEpsilon
+           (inject_Q 0) (inject_Q 1)
+           CReal_plus CReal_opp CReal_mult
+           CReal_isRing CReal_isRingExt CRealLt_0_1
+           CReal_plus_lt_compat_l CReal_plus_lt_reg_l
+           CReal_mult_lt_0_compat
+           CReal_inv CReal_inv_l CReal_inv_0_lt_compat
+           inject_Q inject_Q_plus inject_Q_mult
+           inject_Q_one inject_Q_lt lt_inject_Q
+           CRealQ_dense Rup_pos).
+  - intros. destruct (Rcauchy_complete xn) as [l cv].
+    intro n. destruct (H n). exists x. intros.
+    specialize (a i j H0 H1) as [a b]. split. 2: exact b.
+    rewrite <- opp_inject_Q.
+    setoid_replace (-(1#n))%Q with (-1#n)%Q. exact a. reflexivity.
+    exists l. intros p. destruct (cv p).
+    exists x. intros. specialize (a i H0). split. 2: apply a.
+    unfold orderLe.
+    intro abs. setoid_replace (-1#p)%Q with (-(1#p))%Q in abs.
+    rewrite opp_inject_Q in abs. destruct a. contradiction.
+    reflexivity.
+Defined.
diff --git a/theories/Reals/ConstructiveRealsMorphisms.v b/theories/Reals/ConstructiveRealsMorphisms.v
index 0d3027d475..7954e9a96c 100644
--- a/theories/Reals/ConstructiveRealsMorphisms.v
+++ b/theories/Reals/ConstructiveRealsMorphisms.v
@@ -29,7 +29,7 @@ Require Import QArith.
 Require Import Qabs.
 Require Import ConstructiveReals.
 Require Import ConstructiveCauchyRealsMult.
-Require Import ConstructiveRIneq.
+Require Import ConstructiveRcomplete.
 
 
 Record ConstructiveRealsMorphism (R1 R2 : ConstructiveReals) : Set :=
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index 3b108b485a..7813c7b975 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -13,7 +13,8 @@
 (** * Basic lemmas for the classical real numbers        *)
 (*********************************************************)
 
-Require Import ConstructiveRIneq.
+Require Import ConstructiveCauchyReals.
+Require Import ConstructiveCauchyRealsMult.
 Require Export Raxioms.
 Require Import Rpow_def.
 Require Import Zpower.
@@ -457,11 +458,13 @@ Qed.
 Lemma Rplus_eq_0_l :
   forall r1 r2, 0 <= r1 -> 0 <= r2 -> r1 + r2 = 0 -> r1 = 0.
 Proof.
-  intros. apply Rquot1. rewrite Rrepr_0.
-  apply (Rplus_eq_0_l (Rrepr r1) (Rrepr r2)).
-  rewrite Rrepr_le, Rrepr_0 in H. exact H.
-  rewrite Rrepr_le, Rrepr_0 in H0. exact H0.
-  rewrite <- Rrepr_plus, H1, Rrepr_0. reflexivity.
+  intros a b H [H0| H0] H1; auto with real.
+    absurd (0 < a + b).
+      rewrite H1; auto with real.
+      apply Rle_lt_trans with (a + 0).
+        rewrite Rplus_0_r; assumption.
+        auto using Rplus_lt_compat_l with real.
+    rewrite <- H0, Rplus_0_r in H1; assumption.
 Qed.
 
 Lemma Rplus_eq_R0 :
@@ -541,9 +544,10 @@ Qed.
 (**********)
 Lemma Rmult_eq_reg_l : forall r r1 r2, r * r1 = r * r2 -> r <> 0 -> r1 = r2.
 Proof.
-  intros. apply Rquot1. apply (Rmult_eq_reg_l (Rrepr r)).
-  rewrite <- Rrepr_mult, <- Rrepr_mult, H. reflexivity.
+  intros. apply Rquot1. apply (CReal_mult_eq_reg_l (Rrepr r)).
   apply Rrepr_appart in H0. rewrite Rrepr_0 in H0. exact H0.
+  apply Rrepr_appart in H0.
+  rewrite <- Rrepr_mult, <- Rrepr_mult, H. reflexivity.
 Qed.
 
 Lemma Rmult_eq_reg_r : forall r r1 r2, r1 * r = r2 * r -> r <> 0 -> r1 = r2.
@@ -996,16 +1000,16 @@ Qed.
 
 Lemma Rplus_lt_reg_l : forall r r1 r2, r + r1 < r + r2 -> r1 < r2.
 Proof.
-  intros. rewrite Rlt_def. apply Rlt_forget. apply (Rplus_lt_reg_l (Rrepr r)).
+  intros. rewrite Rlt_def. apply CRealLtForget. apply (CReal_plus_lt_reg_l (Rrepr r)).
   rewrite <- Rrepr_plus, <- Rrepr_plus.
-  rewrite Rlt_def in H. apply Rlt_epsilon. exact H.
+  rewrite Rlt_def in H. apply CRealLtEpsilon. exact H.
 Qed.
 
 Lemma Rplus_lt_reg_r : forall r r1 r2, r1 + r < r2 + r -> r1 < r2.
 Proof.
-  intros. rewrite Rlt_def. apply Rlt_forget. apply (Rplus_lt_reg_r (Rrepr r)).
+  intros. rewrite Rlt_def. apply CRealLtForget. apply (CReal_plus_lt_reg_r (Rrepr r)).
   rewrite <- Rrepr_plus, <- Rrepr_plus. rewrite Rlt_def in H.
-  apply Rlt_epsilon. exact H.
+  apply CRealLtEpsilon. exact H.
 Qed.
 
 Lemma Rplus_le_reg_l : forall r r1 r2, r + r1 <= r + r2 -> r1 <= r2.
@@ -1076,18 +1080,18 @@ Qed.
 Lemma Ropp_gt_lt_contravar : forall r1 r2, r1 > r2 -> - r1 < - r2.
 Proof.
   intros. rewrite Rlt_def. rewrite Rrepr_opp, Rrepr_opp.
-  apply Rlt_forget.
-  apply Ropp_gt_lt_contravar. unfold Rgt in H.
-  rewrite Rlt_def in H. apply Rlt_epsilon. exact H.
+  apply CRealLtForget.
+  apply CReal_opp_gt_lt_contravar. unfold Rgt in H.
+  rewrite Rlt_def in H. apply CRealLtEpsilon. exact H.
 Qed.
 Hint Resolve Ropp_gt_lt_contravar : core.
 
 Lemma Ropp_lt_gt_contravar : forall r1 r2, r1 < r2 -> - r1 > - r2.
 Proof.
   intros. unfold Rgt. rewrite Rlt_def. rewrite Rrepr_opp, Rrepr_opp.
-  apply Rlt_forget.
-  apply Ropp_lt_gt_contravar. rewrite Rlt_def in H.
-  apply Rlt_epsilon. exact H.
+  apply CRealLtForget.
+  apply CReal_opp_gt_lt_contravar. rewrite Rlt_def in H.
+  apply CRealLtEpsilon. exact H.
 Qed.
 Hint Resolve Ropp_lt_gt_contravar: real.
 
@@ -1239,10 +1243,11 @@ Lemma Rmult_le_compat :
   forall r1 r2 r3 r4,
     0 <= r1 -> 0 <= r3 -> r1 <= r2 -> r3 <= r4 -> r1 * r3 <= r2 * r4.
 Proof.
-  intros. rewrite Rrepr_le, Rrepr_mult, Rrepr_mult.
-  apply Rmult_le_compat. rewrite <- Rrepr_0, <- Rrepr_le. exact H.
-  rewrite <- Rrepr_0, <- Rrepr_le. exact H0.
-  rewrite <- Rrepr_le. exact H1. rewrite <- Rrepr_le. exact H2.
+  intros x y z t H' H'0 H'1 H'2.
+  apply Rle_trans with (r2 := x * t); auto with real.
+  repeat rewrite (fun x => Rmult_comm x t).
+  apply Rmult_le_compat_l; auto.
+  apply Rle_trans with z; auto.
 Qed.
 Hint Resolve Rmult_le_compat: real.
 
@@ -1307,18 +1312,20 @@ Qed.
 
 Lemma Rmult_lt_reg_l : forall r r1 r2, 0 < r -> r * r1 < r * r2 -> r1 < r2.
 Proof.
-  intros. rewrite Rlt_def in H,H0. rewrite Rlt_def. apply Rlt_forget.
-  apply (Rmult_lt_reg_l (Rrepr r)).
-  rewrite <- Rrepr_0. apply Rlt_epsilon. exact H.
-  rewrite <- Rrepr_mult, <- Rrepr_mult. apply Rlt_epsilon. exact H0.
+  intros z x y H H0.
+  case (Rtotal_order x y); intros Eq0; auto; elim Eq0; clear Eq0; intros Eq0.
+  rewrite Eq0 in H0; exfalso; apply (Rlt_irrefl (z * y)); auto.
+  generalize (Rmult_lt_compat_l z y x H Eq0); intro; exfalso;
+    generalize (Rlt_trans (z * x) (z * y) (z * x) H0 H1);
+      intro; apply (Rlt_irrefl (z * x)); auto.
 Qed.
 
 Lemma Rmult_lt_reg_r : forall r r1 r2 : R, 0 < r -> r1 * r < r2 * r -> r1 < r2.
 Proof.
-  intros. rewrite Rlt_def. rewrite Rlt_def in H, H0.
-  apply Rlt_forget. apply (Rmult_lt_reg_r (Rrepr r)).
-  rewrite <- Rrepr_0. apply Rlt_epsilon. exact H.
-  rewrite <- Rrepr_mult, <- Rrepr_mult. apply Rlt_epsilon. exact H0.
+  intros.
+  apply Rmult_lt_reg_l with r.
+  exact H.
+  now rewrite 2!(Rmult_comm r).
 Qed.
 
 Lemma Rmult_gt_reg_l : forall r r1 r2, 0 < r -> r * r1 < r * r2 -> r1 < r2.
@@ -1326,10 +1333,14 @@ Proof. eauto using Rmult_lt_reg_l with rorders. Qed.
 
 Lemma Rmult_le_reg_l : forall r r1 r2, 0 < r -> r * r1 <= r * r2 -> r1 <= r2.
 Proof.
-  intros. rewrite Rrepr_le. rewrite Rlt_def in H. apply (Rmult_le_reg_l (Rrepr r)).
-  rewrite <- Rrepr_0. apply Rlt_epsilon. exact H.
-  rewrite <- Rrepr_mult, <- Rrepr_mult.
-  rewrite <- Rrepr_le. exact H0.
+  intros z x y H H0; case H0; auto with real.
+  intros H1; apply Rlt_le.
+  apply Rmult_lt_reg_l with (r := z); auto.
+  intros H1; replace x with (/ z * (z * x)); auto with real.
+  replace y with (/ z * (z * y)).
+  rewrite H1; auto with real.
+  rewrite <- Rmult_assoc; rewrite Rinv_l; auto with real.
+  rewrite <- Rmult_assoc; rewrite Rinv_l; auto with real.
 Qed.
 
 Lemma Rmult_le_reg_r : forall r r1 r2, 0 < r -> r1 * r <= r2 * r -> r1 <= r2.
@@ -1574,9 +1585,11 @@ Qed.
 (**********)
 Lemma plus_INR : forall n m:nat, INR (n + m) = INR n + INR m.
 Proof.
-  intros. apply Rquot1.
-  rewrite Rrepr_INR, Rrepr_plus, plus_INR,
-  <- Rrepr_INR, <- Rrepr_INR. reflexivity.
+  intros n m; induction  n as [| n Hrecn].
+  simpl; auto with real.
+  replace (S n + m)%nat with (S (n + m)); auto with arith.
+  repeat rewrite S_INR.
+  rewrite Hrecn; ring.
 Qed.
 Hint Resolve plus_INR: real.
 
@@ -1645,8 +1658,16 @@ Hint Resolve pos_INR: real.
 
 Lemma INR_lt : forall n m:nat, INR n < INR m -> (n < m)%nat.
 Proof.
-  intros. apply INR_lt. rewrite Rlt_def in H.
-  rewrite Rrepr_INR, Rrepr_INR in H. apply Rlt_epsilon. exact H.
+  intros n m. revert n.
+  induction m ; intros n H.
+  - elim (Rlt_irrefl 0).
+    apply Rle_lt_trans with (2 := H).
+    apply pos_INR.
+  - destruct n as [|n].
+    apply Nat.lt_0_succ.
+    apply lt_n_S, IHm.
+    rewrite 2!S_INR in H.
+    apply Rplus_lt_reg_r with (1 := H).
 Qed.
 Hint Resolve INR_lt: real.
 
@@ -1680,8 +1701,11 @@ Hint Resolve not_0_INR: real.
 
 Lemma not_INR : forall n m:nat, n <> m -> INR n <> INR m.
 Proof.
-  intros. apply Rappart_repr. rewrite Rrepr_INR, Rrepr_INR.
-  apply not_INR. exact H.
+  intros n m H; case (le_or_lt n m); intros H1.
+  case (le_lt_or_eq _ _ H1); intros H2.
+  apply Rlt_dichotomy_converse; auto with real.
+  exfalso; auto.
+  apply not_eq_sym; apply Rlt_dichotomy_converse; auto with real.
 Qed.
 Hint Resolve not_INR: real.
 
@@ -1721,8 +1745,17 @@ Qed.
 
 Lemma INR_IPR : forall p, INR (Pos.to_nat p) = IPR p.
 Proof.
-  intros. apply Rquot1. rewrite Rrepr_INR, Rrepr_IPR.
-  apply INR_IPR.
+  assert (H: forall p, 2 * INR (Pos.to_nat p) = IPR_2 p).
+    induction p as [p|p|] ; simpl IPR_2.
+    rewrite Pos2Nat.inj_xI, S_INR, mult_INR, <- IHp.
+    now rewrite (Rplus_comm (2 * _)).
+    now rewrite Pos2Nat.inj_xO, mult_INR, <- IHp.
+    apply Rmult_1_r.
+  intros [p|p|] ; unfold IPR.
+  rewrite Pos2Nat.inj_xI, S_INR, mult_INR, <- H.
+  apply Rplus_comm.
+  now rewrite Pos2Nat.inj_xO, mult_INR, <- H.
+  easy.
 Qed.
 
 (**********)
@@ -1737,15 +1770,26 @@ Qed.
 Lemma plus_IZR_NEG_POS :
   forall p q:positive, IZR (Zpos p + Zneg q) = IZR (Zpos p) + IZR (Zneg q).
 Proof.
-  intros. apply Rquot1. rewrite Rrepr_plus.
-  do 3 rewrite Rrepr_IZR. apply plus_IZR_NEG_POS.
+  intros p q; simpl. rewrite Z.pos_sub_spec.
+  case Pos.compare_spec; intros H; unfold IZR.
+  subst. ring.
+  rewrite <- 3!INR_IPR, Pos2Nat.inj_sub by trivial.
+  rewrite minus_INR by (now apply lt_le_weak, Pos2Nat.inj_lt).
+  ring.
+  rewrite <- 3!INR_IPR, Pos2Nat.inj_sub by trivial.
+  rewrite minus_INR by (now apply lt_le_weak, Pos2Nat.inj_lt).
+  ring.
 Qed.
 
 (**********)
 Lemma plus_IZR : forall n m:Z, IZR (n + m) = IZR n + IZR m.
 Proof.
-  intros. apply Rquot1.
-  rewrite Rrepr_plus. do 3 rewrite Rrepr_IZR. apply plus_IZR.
+  intro z; destruct z; intro t; destruct t; intros; auto with real.
+  simpl. unfold IZR. rewrite <- 3!INR_IPR, Pos2Nat.inj_add. apply plus_INR.
+  apply plus_IZR_NEG_POS.
+  rewrite Z.add_comm; rewrite Rplus_comm; apply plus_IZR_NEG_POS.
+  simpl. unfold IZR. rewrite <- 3!INR_IPR, Pos2Nat.inj_add, plus_INR.
+  apply Ropp_plus_distr.
 Qed.
 
 (**********)
@@ -1755,21 +1799,14 @@ Proof.
     unfold IZR; intros m n; rewrite <- 3!INR_IPR, Pos2Nat.inj_mul, mult_INR; ring.
 Qed.
 
-Lemma Rrepr_pow : forall (x : R) (n : nat),
-    (ConstructiveRIneq.Req (Rrepr (pow x n))
-                           (ConstructiveRIneq.pow (Rrepr x) n)).
-Proof.
-  intro x. induction n.
-  - apply Rrepr_1.
-  - simpl. rewrite Rrepr_mult, <- IHn. reflexivity.
-Qed.
-
 Lemma pow_IZR : forall z n, pow (IZR z) n = IZR (Z.pow z (Z.of_nat n)).
 Proof.
-  intros. apply Rquot1.
-  rewrite Rrepr_IZR, Rrepr_pow.
-  rewrite (Rpow_eq_compat _ _ n (Rrepr_IZR z)).
-  apply pow_IZR.
+ intros z [|n];simpl;trivial.
+ rewrite Zpower_pos_nat.
+ rewrite SuccNat2Pos.id_succ. unfold Zpower_nat;simpl.
+ rewrite mult_IZR.
+ induction n;simpl;trivial.
+ rewrite mult_IZR;ring[IHn].
 Qed.
 
 (**********)
@@ -1803,23 +1840,34 @@ Qed.
 (**********)
 Lemma lt_0_IZR : forall n:Z, 0 < IZR n -> (0 < n)%Z.
 Proof.
-  intros. apply lt_0_IZR. rewrite <- Rrepr_0, <- Rrepr_IZR.
-  rewrite Rlt_def in H. apply Rlt_epsilon. exact H.
+  intro z; case z; simpl; intros.
+  elim (Rlt_irrefl _ H).
+  easy.
+  elim (Rlt_not_le _ _ H).
+  unfold IZR.
+  rewrite <- INR_IPR.
+  auto with real.
 Qed.
 
 (**********)
 Lemma lt_IZR : forall n m:Z, IZR n < IZR m -> (n < m)%Z.
 Proof.
-  intros. apply lt_IZR.
-  rewrite <- Rrepr_IZR, <- Rrepr_IZR. rewrite Rlt_def in H.
-  apply Rlt_epsilon. exact H.
+  intros z1 z2 H; apply Z.lt_0_sub.
+  apply lt_0_IZR.
+  rewrite <- Z_R_minus.
+  exact (Rgt_minus (IZR z2) (IZR z1) H).
 Qed.
 
 (**********)
 Lemma eq_IZR_R0 : forall n:Z, IZR n = 0 -> n = 0%Z.
 Proof.
-  intros. apply eq_IZR_R0.
-  rewrite <- Rrepr_0, <- Rrepr_IZR, H. reflexivity.
+  intro z; destruct z; simpl; intros; auto with zarith.
+  elim Rgt_not_eq with (2 := H).
+  unfold IZR. rewrite <- INR_IPR.
+  apply lt_0_INR, Pos2Nat.is_pos.
+  elim Rlt_not_eq with (2 := H).
+  unfold IZR. rewrite <- INR_IPR.
+  apply Ropp_lt_gt_0_contravar, lt_0_INR, Pos2Nat.is_pos.
 Qed.
 
 (**********)
@@ -1895,21 +1943,26 @@ Hint Extern 0 (IZR _ <> IZR _) => apply IZR_neq, Zeq_bool_neq, eq_refl : real.
 
 Lemma one_IZR_lt1 : forall n:Z, -1 < IZR n < 1 -> n = 0%Z.
 Proof.
-  intros. apply one_IZR_lt1. do 2 rewrite Rlt_def in H. split.
-  rewrite <- Rrepr_IZR, <- Rrepr_1, <- Rrepr_opp.
-  apply Rlt_epsilon. apply H.
-  rewrite <- Rrepr_IZR, <- Rrepr_1. apply Rlt_epsilon. apply H.
+  intros z [H1 H2].
+  apply Z.le_antisymm.
+  apply Z.lt_succ_r; apply lt_IZR; trivial.
+  change 0%Z with (Z.succ (-1)).
+  apply Z.le_succ_l; apply lt_IZR; trivial.
 Qed.
 
 Lemma one_IZR_r_R1 :
   forall r (n m:Z), r < IZR n <= r + 1 -> r < IZR m <= r + 1 -> n = m.
 Proof.
-  intros. rewrite Rlt_def in H, H0. apply (one_IZR_r_R1 (Rrepr r)); split.
-  rewrite <- Rrepr_IZR. apply Rlt_epsilon. apply H.
-  rewrite <- Rrepr_IZR, <- Rrepr_1, <- Rrepr_plus, <- Rrepr_le.
-  apply H. rewrite <- Rrepr_IZR. apply Rlt_epsilon. apply H0.
-  rewrite <- Rrepr_IZR, <- Rrepr_1, <- Rrepr_plus, <- Rrepr_le.
-  apply H0.
+  intros r z x [H1 H2] [H3 H4].
+  cut ((z - x)%Z = 0%Z); auto with zarith.
+  apply one_IZR_lt1.
+  rewrite <- Z_R_minus; split.
+  replace (-1) with (r - (r + 1)).
+  unfold Rminus; apply Rplus_lt_le_compat; auto with real.
+  ring.
+  replace 1 with (r + 1 - r).
+  unfold Rminus; apply Rplus_le_lt_compat; auto with real.
+  ring.
 Qed.
 
 
@@ -1942,13 +1995,13 @@ Qed.
 Lemma Rinv_le_contravar :
   forall x y, 0 < x -> x <= y -> / y <= / x.
 Proof.
-  intros. apply Rrepr_le. assert (y <> 0).
-  intro abs. subst y. apply (Rlt_irrefl 0). exact (Rlt_le_trans 0 x 0 H H0).
-  apply Rrepr_appart in H1.
-  rewrite Rrepr_0 in H1. rewrite Rlt_def in H. rewrite Rrepr_0 in H.
-  apply Rlt_epsilon in H.
-  rewrite (Rrepr_inv y H1), (Rrepr_inv x (inr H)).
-  apply Rinv_le_contravar. rewrite <- Rrepr_le. exact H0.
+  intros x y H1 [H2|H2].
+  apply Rlt_le.
+  apply Rinv_lt_contravar with (2 := H2).
+  apply Rmult_lt_0_compat with (1 := H1).
+  now apply Rlt_trans with x.
+  rewrite H2.
+  apply Rle_refl.
 Qed.
 
 Lemma Rle_Rinv : forall x y:R, 0 < x -> 0 < y -> x <= y -> / y <= / x.
@@ -2012,10 +2065,18 @@ Qed.
 Lemma le_epsilon :
   forall r1 r2, (forall eps:R, 0 < eps -> r1 <= r2 + eps) -> r1 <= r2.
 Proof.
-  intros. rewrite Rrepr_le. apply le_epsilon.
-  intros. rewrite <- (Rquot2 eps), <- Rrepr_plus.
-  rewrite <- Rrepr_le. apply H. rewrite Rlt_def.
-  rewrite Rquot2, Rrepr_0. apply Rlt_forget. exact H0.
+  intros x y H.
+  destruct (Rle_or_lt x y) as [H1|H1].
+  exact H1.
+  apply Rplus_le_reg_r with x.
+  replace (y + x) with (2 * (y + (x - y) * / 2)) by field.
+  replace (x + x) with (2 * x) by ring.
+  apply Rmult_le_compat_l.
+  now apply (IZR_le 0 2).
+  apply H.
+  apply Rmult_lt_0_compat.
+  now apply Rgt_minus.
+  apply Rinv_0_lt_compat, Rlt_0_2.
 Qed.
 
 (**********)
diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v
index d856d1c7fe..be283fb7cf 100644
--- a/theories/Reals/Raxioms.v
+++ b/theories/Reals/Raxioms.v
@@ -20,10 +20,12 @@
 (*********************************************************)
 
 Require Export ZArith_base.
-Require Import ConstructiveRIneq.
+Require Import ClassicalDedekindReals.
+Require Import ConstructiveCauchyReals.
+Require Import ConstructiveCauchyRealsMult.
+Require Import ConstructiveRcomplete.
 Require Import ConstructiveRealsLUB.
 Require Export Rdefinitions.
-Declare Scope R_scope.
 Local Open Scope R_scope.
 
 (*********************************************************)
@@ -34,7 +36,7 @@ Local Open Scope R_scope.
 (** **   Addition                                        *)
 (*********************************************************)
 
-Open Scope R_scope_constr.
+Open Scope CReal_scope.
 
 Lemma Rrepr_0 : Rrepr 0 == 0.
 Proof.
@@ -58,7 +60,7 @@ Qed.
 
 Lemma Rrepr_minus : forall x y:R, Rrepr (x - y) == Rrepr x - Rrepr y.
 Proof.
-  intros. unfold Rminus, CRminus.
+  intros. unfold Rminus, CReal_minus.
   rewrite Rrepr_plus, Rrepr_opp. reflexivity.
 Qed.
 
@@ -72,10 +74,10 @@ Lemma Rrepr_inv : forall (x:R) (xnz : Rrepr x # 0),
 Proof.
   intros. rewrite RinvImpl.Rinv_def. destruct (Req_appart_dec x R0).
   - exfalso. subst x. destruct xnz.
-    rewrite Rrepr_0 in c. exact (Rlt_irrefl 0 c).
-    rewrite Rrepr_0 in c. exact (Rlt_irrefl 0 c).
-  - rewrite Rquot2. apply (Rmult_eq_reg_l (Rrepr x)). 2: exact xnz.
-    rewrite Rmult_comm, (Rmult_comm (Rrepr x)), Rinv_l, Rinv_l.
+    rewrite Rrepr_0 in c. exact (CRealLt_irrefl 0 c).
+    rewrite Rrepr_0 in c. exact (CRealLt_irrefl 0 c).
+  - rewrite Rquot2. apply (CReal_mult_eq_reg_l (Rrepr x)). exact xnz.
+    rewrite CReal_mult_comm, (CReal_mult_comm (Rrepr x)), CReal_inv_l, CReal_inv_l.
     reflexivity.
 Qed.
 
@@ -83,12 +85,12 @@ Lemma Rrepr_le : forall x y:R, (x <= y)%R <-> Rrepr x <= Rrepr y.
 Proof.
   split.
   - intros [H|H] abs. rewrite RbaseSymbolsImpl.Rlt_def in H.
-    apply Rlt_epsilon in H.
-    exact (Rlt_asym (Rrepr x) (Rrepr y) H abs).
-    destruct H. exact (Rlt_asym (Rrepr x) (Rrepr x) abs abs).
+    apply CRealLtEpsilon in H.
+    exact (CRealLt_asym (Rrepr x) (Rrepr y) H abs).
+    destruct H. exact (CRealLt_asym (Rrepr x) (Rrepr x) abs abs).
   - intros. destruct (total_order_T x y). destruct s.
     left. exact r. right. exact e.
-    rewrite RbaseSymbolsImpl.Rlt_def in r. apply Rlt_epsilon in r. contradiction.
+    rewrite RbaseSymbolsImpl.Rlt_def in r. apply CRealLtEpsilon in r. contradiction.
 Qed.
 
 Lemma Rrepr_appart : forall x y:R,
@@ -96,26 +98,26 @@ Lemma Rrepr_appart : forall x y:R,
 Proof.
   intros. destruct (total_order_T x y). destruct s.
   left. rewrite RbaseSymbolsImpl.Rlt_def in r.
-  apply Rlt_epsilon. exact r. contradiction.
+  apply CRealLtEpsilon. exact r. contradiction.
   right. rewrite RbaseSymbolsImpl.Rlt_def in r.
-  apply Rlt_epsilon. exact r.
+  apply CRealLtEpsilon. exact r.
 Qed.
 
 Lemma Rappart_repr : forall x y:R,
     Rrepr x # Rrepr y -> (x <> y)%R.
 Proof.
   intros x y [H|H] abs.
-  destruct abs. exact (Rlt_asym (Rrepr x) (Rrepr x) H H).
-  destruct abs. exact (Rlt_asym (Rrepr x) (Rrepr x) H H).
+  destruct abs. exact (CRealLt_asym (Rrepr x) (Rrepr x) H H).
+  destruct abs. exact (CRealLt_asym (Rrepr x) (Rrepr x) H H).
 Qed.
 
-Close Scope R_scope_constr.
+Close Scope CReal_scope.
 
 
 (**********)
 Lemma Rplus_comm : forall r1 r2:R, r1 + r2 = r2 + r1.
 Proof.
-  intros. apply Rquot1. do 2 rewrite Rrepr_plus. apply Rplus_comm.
+  intros. apply Rquot1. do 2 rewrite Rrepr_plus. apply CReal_plus_comm.
 Qed.
 Hint Resolve Rplus_comm: real.
 
@@ -123,7 +125,7 @@ Hint Resolve Rplus_comm: real.
 Lemma Rplus_assoc : forall r1 r2 r3:R, r1 + r2 + r3 = r1 + (r2 + r3).
 Proof.
   intros. apply Rquot1. repeat rewrite Rrepr_plus.
-  apply Rplus_assoc.
+  apply CReal_plus_assoc.
 Qed.
 Hint Resolve Rplus_assoc: real.
 
@@ -131,7 +133,7 @@ Hint Resolve Rplus_assoc: real.
 Lemma Rplus_opp_r : forall r:R, r + - r = 0.
 Proof.
   intros. apply Rquot1. rewrite Rrepr_plus, Rrepr_opp, Rrepr_0.
-  apply Rplus_opp_r.
+  apply CReal_plus_opp_r.
 Qed.
 Hint Resolve Rplus_opp_r: real.
 
@@ -139,7 +141,7 @@ Hint Resolve Rplus_opp_r: real.
 Lemma Rplus_0_l : forall r:R, 0 + r = r.
 Proof.
   intros. apply Rquot1. rewrite Rrepr_plus, Rrepr_0.
-  apply Rplus_0_l.
+  apply CReal_plus_0_l.
 Qed.
 Hint Resolve Rplus_0_l: real.
 
@@ -150,7 +152,7 @@ Hint Resolve Rplus_0_l: real.
 (**********)
 Lemma Rmult_comm : forall r1 r2:R, r1 * r2 = r2 * r1.
 Proof.
-  intros. apply Rquot1. do 2 rewrite Rrepr_mult. apply Rmult_comm.
+  intros. apply Rquot1. do 2 rewrite Rrepr_mult. apply CReal_mult_comm.
 Qed.
 Hint Resolve Rmult_comm: real.
 
@@ -158,7 +160,7 @@ Hint Resolve Rmult_comm: real.
 Lemma Rmult_assoc : forall r1 r2 r3:R, r1 * r2 * r3 = r1 * (r2 * r3).
 Proof.
   intros. apply Rquot1. repeat rewrite Rrepr_mult.
-  apply Rmult_assoc.
+  apply CReal_mult_assoc.
 Qed.
 Hint Resolve Rmult_assoc: real.
 
@@ -167,7 +169,7 @@ Lemma Rinv_l : forall r:R, r <> 0 -> / r * r = 1.
 Proof.
   intros. rewrite RinvImpl.Rinv_def; destruct (Req_appart_dec r R0).
   - contradiction.
-  - apply Rquot1. rewrite Rrepr_mult, Rquot2, Rrepr_1. apply Rinv_l.
+  - apply Rquot1. rewrite Rrepr_mult, Rquot2, Rrepr_1. apply CReal_inv_l.
 Qed.
 Hint Resolve Rinv_l: real.
 
@@ -175,7 +177,7 @@ Hint Resolve Rinv_l: real.
 Lemma Rmult_1_l : forall r:R, 1 * r = r.
 Proof.
   intros. apply Rquot1. rewrite Rrepr_mult, Rrepr_1.
-  apply Rmult_1_l.
+  apply CReal_mult_1_l.
 Qed.
 Hint Resolve Rmult_1_l: real.
 
@@ -183,17 +185,17 @@ Hint Resolve Rmult_1_l: real.
 Lemma R1_neq_R0 : 1 <> 0.
 Proof.
   intro abs.
-  assert (Req (CRone CR) (CRzero CR)).
+  assert (CRealEq 1%CReal 0%CReal).
   { transitivity (Rrepr 1). symmetry.
-    replace 1%R with (Rabst (CRone CR)).
+    replace 1%R with (Rabst 1%CReal).
     2: unfold IZR,IPR; rewrite RbaseSymbolsImpl.R1_def; reflexivity.
     rewrite Rquot2. reflexivity. transitivity (Rrepr 0).
     rewrite abs. reflexivity.
-    replace 0%R with (Rabst (CRzero CR)).
+    replace 0%R with (Rabst 0%CReal).
     2: unfold IZR; rewrite RbaseSymbolsImpl.R0_def; reflexivity.
     rewrite Rquot2. reflexivity. }
-  pose proof (Rlt_morph (CRzero CR) (CRzero CR) (Req_refl _) (CRone CR) (CRzero CR) H).
-  apply (Rlt_irrefl (CRzero CR)). apply H0. apply Rlt_0_1.
+  pose proof (CRealLt_morph 0%CReal 0%CReal (CRealEq_refl _) 1%CReal 0%CReal H).
+  apply (CRealLt_irrefl 0%CReal). apply H0. apply CRealLt_0_1.
 Qed.
 Hint Resolve R1_neq_R0: real.
 
@@ -207,7 +209,7 @@ Lemma
 Proof.
   intros. apply Rquot1.
   rewrite Rrepr_mult, Rrepr_plus, Rrepr_plus, Rrepr_mult, Rrepr_mult.
-  apply Rmult_plus_distr_l.
+  apply CReal_mult_plus_distr_l.
 Qed.
 Hint Resolve Rmult_plus_distr_l: real.
 
@@ -223,35 +225,35 @@ Hint Resolve Rmult_plus_distr_l: real.
 Lemma Rlt_asym : forall r1 r2:R, r1 < r2 -> ~ r2 < r1.
 Proof.
   intros. intro abs. rewrite RbaseSymbolsImpl.Rlt_def in H, abs.
-  apply Rlt_epsilon in H. apply Rlt_epsilon in abs.
-  apply (Rlt_asym (Rrepr r1) (Rrepr r2)); assumption.
+  apply CRealLtEpsilon in H. apply CRealLtEpsilon in abs.
+  apply (CRealLt_asym (Rrepr r1) (Rrepr r2)); assumption.
 Qed.
 
 (**********)
 Lemma Rlt_trans : forall r1 r2 r3:R, r1 < r2 -> r2 < r3 -> r1 < r3.
 Proof.
   intros. rewrite RbaseSymbolsImpl.Rlt_def. rewrite RbaseSymbolsImpl.Rlt_def in H, H0.
-  apply Rlt_epsilon in H. apply Rlt_epsilon in H0.
-  apply Rlt_forget.
-  apply (Rlt_trans (Rrepr r1) (Rrepr r2) (Rrepr r3)); assumption.
+  apply CRealLtEpsilon in H. apply CRealLtEpsilon in H0.
+  apply CRealLtForget.
+  apply (CReal_lt_trans (Rrepr r1) (Rrepr r2) (Rrepr r3)); assumption.
 Qed.
 
 (**********)
 Lemma Rplus_lt_compat_l : forall r r1 r2:R, r1 < r2 -> r + r1 < r + r2.
 Proof.
   intros. rewrite RbaseSymbolsImpl.Rlt_def. rewrite RbaseSymbolsImpl.Rlt_def in H.
-  do 2 rewrite Rrepr_plus. apply Rlt_forget.
-  apply Rplus_lt_compat_l. apply Rlt_epsilon. exact H.
+  do 2 rewrite Rrepr_plus. apply CRealLtForget.
+  apply CReal_plus_lt_compat_l. apply CRealLtEpsilon. exact H.
 Qed.
 
 (**********)
 Lemma Rmult_lt_compat_l : forall r r1 r2:R, 0 < r -> r1 < r2 -> r * r1 < r * r2.
 Proof.
   intros. rewrite RbaseSymbolsImpl.Rlt_def. rewrite RbaseSymbolsImpl.Rlt_def in H.
-  do 2 rewrite Rrepr_mult. apply Rlt_forget. apply Rmult_lt_compat_l.
-  rewrite <- (Rquot2 (CRzero CR)). unfold IZR in H.
-  rewrite RbaseSymbolsImpl.R0_def in H. apply Rlt_epsilon. exact H.
-  rewrite RbaseSymbolsImpl.Rlt_def in H0. apply Rlt_epsilon. exact H0.
+  do 2 rewrite Rrepr_mult. apply CRealLtForget. apply CReal_mult_lt_compat_l.
+  rewrite <- (Rquot2 0%CReal). unfold IZR in H.
+  rewrite RbaseSymbolsImpl.R0_def in H. apply CRealLtEpsilon. exact H.
+  rewrite RbaseSymbolsImpl.Rlt_def in H0. apply CRealLtEpsilon. exact H0.
 Qed.
 
 Hint Resolve Rlt_asym Rplus_lt_compat_l Rmult_lt_compat_l: real.
@@ -274,119 +276,133 @@ Arguments INR n%nat.
 (**********************************************************)
 
 Lemma Rrepr_INR : forall n : nat,
-    Req (Rrepr (INR n)) (ConstructiveRIneq.INR n).
+    CRealEq (Rrepr (INR n)) (inject_Z (Z.of_nat n)).
 Proof.
   induction n.
   - apply Rrepr_0.
-  - simpl. destruct n. apply Rrepr_1.
-    rewrite Rrepr_plus, <- IHn, Rrepr_1. reflexivity.
+  - replace (Z.of_nat (S n)) with (Z.of_nat n + 1)%Z.
+    simpl. destruct n. apply Rrepr_1.
+    rewrite Rrepr_plus,inject_Z_plus, <- IHn, Rrepr_1. reflexivity.
+    replace 1%Z with (Z.of_nat 1). rewrite <- (Nat2Z.inj_add n 1).
+    apply f_equal. rewrite Nat.add_comm. reflexivity. reflexivity.
 Qed.
 
 Lemma Rrepr_IPR2 : forall n : positive,
-    Req (Rrepr (IPR_2 n)) (ConstructiveRIneq.IPR_2 n).
+    CRealEq (Rrepr (IPR_2 n)) (inject_Z (Z.pos (n~0))).
 Proof.
   induction n.
-  - unfold IPR_2, ConstructiveRIneq.IPR_2.
-    rewrite RbaseSymbolsImpl.R1_def, Rrepr_mult, Rrepr_plus, Rrepr_plus, <- IHn.
-    unfold IPR_2.
-    rewrite Rquot2. rewrite RbaseSymbolsImpl.R1_def. reflexivity.
-  - unfold IPR_2, ConstructiveRIneq.IPR_2.
-    rewrite Rrepr_mult, Rrepr_plus, <- IHn.
-    rewrite RbaseSymbolsImpl.R1_def. rewrite Rquot2.
-    unfold IPR_2. rewrite RbaseSymbolsImpl.R1_def. reflexivity.
-  - unfold IPR_2, ConstructiveRIneq.IPR_2.
-    rewrite RbaseSymbolsImpl.R1_def.
-    rewrite Rrepr_plus, Rquot2. reflexivity.
+  - simpl. replace (Z.pos n~1~0) with ((Z.pos n~0 + 1) + (Z.pos n~0 + 1))%Z.
+    rewrite RbaseSymbolsImpl.R1_def, Rrepr_mult, inject_Z_plus, inject_Z_plus.
+    rewrite Rrepr_plus, Rrepr_plus, <- IHn.
+    rewrite Rquot2, CReal_mult_plus_distr_r, CReal_mult_1_l.
+    rewrite (CReal_plus_comm 1%CReal). repeat rewrite CReal_plus_assoc.
+    apply CReal_plus_morph. reflexivity.
+    reflexivity.
+    repeat rewrite <- Pos2Z.inj_add. apply f_equal.
+    rewrite Pos.add_diag. apply f_equal.
+    rewrite Pos.add_1_r. reflexivity.
+  - simpl. replace (Z.pos n~0~0) with ((Z.pos n~0) + (Z.pos n~0))%Z.
+    rewrite RbaseSymbolsImpl.R1_def, Rrepr_mult, inject_Z_plus.
+    rewrite Rrepr_plus, <- IHn.
+    rewrite Rquot2, CReal_mult_plus_distr_r, CReal_mult_1_l. reflexivity.
+    rewrite <- Pos2Z.inj_add. apply f_equal.
+    rewrite Pos.add_diag. reflexivity.
+  - simpl. rewrite Rrepr_plus, RbaseSymbolsImpl.R1_def, Rquot2.
+    replace 2%Z with (1 + 1)%Z. rewrite inject_Z_plus. reflexivity.
+    reflexivity.
 Qed.
 
 Lemma Rrepr_IPR : forall n : positive,
-    Req (Rrepr (IPR n)) (ConstructiveRIneq.IPR n).
+    CRealEq (Rrepr (IPR n)) (inject_Z (Z.pos n)).
 Proof.
   intro n. destruct n.
-  - unfold IPR, ConstructiveRIneq.IPR.
-    rewrite Rrepr_plus, <- Rrepr_IPR2.
-    rewrite RbaseSymbolsImpl.R1_def. rewrite Rquot2. reflexivity.
-  - unfold IPR, ConstructiveRIneq.IPR.
-    apply Rrepr_IPR2.
+  - unfold IPR. rewrite Rrepr_plus.
+    replace (n~1)%positive with (n~0 + 1)%positive.
+    rewrite Pos2Z.inj_add, inject_Z_plus, <- Rrepr_IPR2, CReal_plus_comm.
+    rewrite RbaseSymbolsImpl.R1_def, Rquot2. reflexivity.
+    rewrite Pos.add_1_r. reflexivity.
+  - apply Rrepr_IPR2.
   - unfold IPR. rewrite RbaseSymbolsImpl.R1_def. apply Rquot2.
 Qed.
 
 Lemma Rrepr_IZR : forall n : Z,
-    Req (Rrepr (IZR n)) (ConstructiveRIneq.IZR n).
+    CRealEq (Rrepr (IZR n)) (inject_Z n).
 Proof.
   intros [|p|n].
   - unfold IZR. rewrite RbaseSymbolsImpl.R0_def. apply Rquot2.
   - apply Rrepr_IPR.
-  - unfold IZR, ConstructiveRIneq.IZR.
-    rewrite <- Rrepr_IPR, Rrepr_opp. reflexivity.
+  - unfold IZR. rewrite Rrepr_opp, Rrepr_IPR. rewrite <- opp_inject_Z.
+    replace (- Z.pos n)%Z with (Z.neg n). reflexivity. reflexivity.
 Qed.
 
 (**********)
 Lemma archimed : forall r:R, IZR (up r) > r /\ IZR (up r) - r <= 1.
 Proof.
   intro r. unfold up.
-  destruct (Rarchimedean (Rrepr r)) as [n nmaj], (total_order_T (IZR n - r) R1).
+  destruct (CRealArchimedean (Rrepr r)) as [n nmaj], (total_order_T (IZR n - r) R1).
   destruct s.
   - split. unfold Rgt. rewrite RbaseSymbolsImpl.Rlt_def. rewrite Rrepr_IZR.
-    apply Rlt_forget. apply nmaj.
+    apply CRealLtForget. apply nmaj.
     unfold Rle. left. exact r0.
   - split. unfold Rgt. rewrite RbaseSymbolsImpl.Rlt_def.
-    rewrite Rrepr_IZR. apply Rlt_forget. apply nmaj. right. exact e.
+    rewrite Rrepr_IZR. apply CRealLtForget. apply nmaj. right. exact e.
   - split.
     + unfold Rgt, Z.pred. rewrite RbaseSymbolsImpl.Rlt_def.
-      rewrite Rrepr_IZR, plus_IZR.
+      rewrite Rrepr_IZR, inject_Z_plus.
       rewrite RbaseSymbolsImpl.Rlt_def in r0. rewrite Rrepr_minus in r0.
       rewrite <- (Rrepr_IZR n).
-      unfold ConstructiveRIneq.IZR, ConstructiveRIneq.IPR.
-      apply Rlt_forget. apply Rlt_epsilon in r0.
-      unfold ConstructiveRIneq.Rminus in r0.
-      apply (ConstructiveRIneq.Rplus_lt_compat_l
-               (ConstructiveRIneq.Rplus (Rrepr r) (ConstructiveRIneq.Ropp (Rrepr R1))))
+      apply CRealLtForget. apply CRealLtEpsilon in r0.
+      unfold CReal_minus in r0.
+      apply (CReal_plus_lt_compat_l
+               (CReal_plus (Rrepr r) (CReal_opp (Rrepr R1))))
         in r0.
-      rewrite ConstructiveRIneq.Rplus_assoc,
-      ConstructiveRIneq.Rplus_opp_l,
-      ConstructiveRIneq.Rplus_0_r,
+      rewrite CReal_plus_assoc,
+      CReal_plus_opp_l,
+      CReal_plus_0_r,
       RbaseSymbolsImpl.R1_def, Rquot2,
-      ConstructiveRIneq.Rplus_comm,
-      ConstructiveRIneq.Rplus_assoc,
-      <- (ConstructiveRIneq.Rplus_assoc (ConstructiveRIneq.Ropp (Rrepr r))),
-      ConstructiveRIneq.Rplus_opp_l,
-      ConstructiveRIneq.Rplus_0_l
+      CReal_plus_comm,
+      CReal_plus_assoc,
+      <- (CReal_plus_assoc (CReal_opp (Rrepr r))),
+      CReal_plus_opp_l,
+      CReal_plus_0_l
         in r0.
-      exact r0.
+      rewrite (opp_inject_Z 1). exact r0.
     + destruct (total_order_T (IZR (Z.pred n) - r) 1). destruct s.
       left. exact r1. right. exact e.
-      exfalso. destruct nmaj as [_ nmaj]. rewrite <- Rrepr_IZR in nmaj.
+      exfalso. destruct nmaj as [_ nmaj].
+      pose proof Rrepr_IZR as iz. unfold inject_Z in iz.
+      rewrite <- iz in nmaj.
       apply (Rlt_asym (IZR n) (r + 2)).
       rewrite RbaseSymbolsImpl.Rlt_def. rewrite Rrepr_plus. rewrite (Rrepr_plus 1 1).
-      apply Rlt_forget.
-      apply (ConstructiveRIneq.Rlt_le_trans
-               _ (ConstructiveRIneq.Rplus (Rrepr r) (ConstructiveRIneq.IZR 2))).
-      apply nmaj.
-      unfold IZR, IPR. rewrite RbaseSymbolsImpl.R1_def, Rquot2. apply Rle_refl.
+      apply CRealLtForget.
+      apply (CReal_lt_le_trans _ _ _ nmaj).
+      unfold IZR, IPR. rewrite RbaseSymbolsImpl.R1_def, Rquot2.
+      rewrite <- (inject_Z_plus 1 1). apply CRealLe_refl.
       clear nmaj.
       unfold Z.pred in r1. rewrite RbaseSymbolsImpl.Rlt_def in r1.
-      rewrite Rrepr_minus, (Rrepr_IZR (n + -1)), plus_IZR,
-      <- (Rrepr_IZR n)
-        in r1.
-      unfold ConstructiveRIneq.IZR, ConstructiveRIneq.IPR in r1.
+      rewrite Rrepr_minus, (Rrepr_IZR (n + -1)) in r1.
+      rewrite inject_Z_plus, <- (Rrepr_IZR n) in r1.
       rewrite RbaseSymbolsImpl.Rlt_def, Rrepr_plus.
-      apply Rlt_epsilon in r1.
-      apply (ConstructiveRIneq.Rplus_lt_compat_l
-               (ConstructiveRIneq.Rplus (Rrepr r) (CRone CR))) in r1.
-      apply Rlt_forget.
-      apply (ConstructiveRIneq.Rle_lt_trans
-               _ (ConstructiveRIneq.Rplus (ConstructiveRIneq.Rplus (Rrepr r) (Rrepr 1)) (CRone CR))).
+      apply CRealLtEpsilon in r1.
+      apply (CReal_plus_lt_compat_l
+               (CReal_plus (Rrepr r) 1%CReal)) in r1.
+      apply CRealLtForget.
+      apply (CReal_le_lt_trans
+               _ (CReal_plus (CReal_plus (Rrepr r) (Rrepr 1)) 1%CReal)).
       rewrite (Rrepr_plus 1 1). unfold IZR, IPR.
-      rewrite RbaseSymbolsImpl.R1_def, (Rquot2 (CRone CR)), <- ConstructiveRIneq.Rplus_assoc.
-      apply Rle_refl.
-      rewrite <- (ConstructiveRIneq.Rplus_comm (Rrepr 1)),
-      <- ConstructiveRIneq.Rplus_assoc,
-      (ConstructiveRIneq.Rplus_comm (Rrepr 1))
+      rewrite RbaseSymbolsImpl.R1_def, (Rquot2 1%CReal), <- CReal_plus_assoc.
+      apply CRealLe_refl.
+      rewrite <- (CReal_plus_comm (Rrepr 1)),
+      <- CReal_plus_assoc,
+      (CReal_plus_comm (Rrepr 1))
         in r1.
-      apply (ConstructiveRIneq.Rlt_le_trans _ _ _ r1).
-      unfold ConstructiveRIneq.Rminus.
-      ring_simplify. apply ConstructiveRIneq.Rle_refl.
+      apply (CReal_lt_le_trans _ _ _ r1).
+      unfold CReal_minus. rewrite (opp_inject_Z 1).
+      rewrite (CReal_plus_comm (Rrepr (IZR n))), CReal_plus_assoc,
+      <- (CReal_plus_assoc 1), <- (CReal_plus_assoc 1), CReal_plus_opp_r.
+      rewrite CReal_plus_0_l, CReal_plus_comm, CReal_plus_assoc,
+      CReal_plus_opp_l, CReal_plus_0_r.
+      apply CRealLe_refl.
 Qed.
 
 (**********************************************************)
@@ -408,29 +424,29 @@ Lemma completeness :
     forall E:R -> Prop,
       bound E -> (exists x : R, E x) -> { m:R | is_lub E m }.
 Proof.
-  intros. pose (fun x:ConstructiveRIneq.R => E (Rabst x)) as Er.
-  assert (forall x y : CRcarrier CR, orderEq (CRcarrier CR) (CRlt CR) x y -> Er x <-> Er y)
+  intros. pose (fun x:CReal => E (Rabst x)) as Er.
+  assert (forall x y : CReal, CRealEq x y -> Er x <-> Er y)
     as Erproper.
   { intros. unfold Er. replace (Rabst x) with (Rabst y). reflexivity.
     apply Rquot1. do 2 rewrite Rquot2. split; apply H1. }
-  assert (exists x : ConstructiveRIneq.R, Er x) as Einhab.
+  assert (exists x : CReal, Er x) as Einhab.
   { destruct H0. exists (Rrepr x). unfold Er.
     replace (Rabst (Rrepr x)) with x. exact H0.
     apply Rquot1. rewrite Rquot2. reflexivity. }
-  assert (exists x : ConstructiveRIneq.R,
-             (forall y:ConstructiveRIneq.R, Er y -> ConstructiveRIneq.Rle y x))
+  assert (exists x : CReal,
+             (forall y:CReal, Er y -> CRealLe y x))
     as Ebound.
   { destruct H. exists (Rrepr x). intros y Ey. rewrite <- (Rquot2 y).
     apply Rrepr_le. apply H. exact Ey. }
-  destruct (CR_sig_lub CR
+  destruct (CR_sig_lub CRealImplem
               Er Erproper sig_forall_dec sig_not_dec Einhab Ebound).
   exists (Rabst x). split.
   intros y Ey. apply Rrepr_le. rewrite Rquot2.
-  unfold ConstructiveRIneq.Rle. apply a.
+  unfold CRealLe. apply a.
   unfold Er. replace (Rabst (Rrepr y)) with y. exact Ey.
   apply Rquot1. rewrite Rquot2. reflexivity.
   intros. destruct a. apply Rrepr_le. rewrite Rquot2.
-  unfold ConstructiveRIneq.Rle. apply H3. intros y Ey.
+  unfold CRealLe. apply H3. intros y Ey.
   intros. rewrite <- (Rquot2 y) in H4.
   apply Rrepr_le in H4. exact H4.
   apply H1, Ey.
diff --git a/theories/Reals/Rdefinitions.v b/theories/Reals/Rdefinitions.v
index b1ce8109ca..35025ba9bc 100644
--- a/theories/Reals/Rdefinitions.v
+++ b/theories/Reals/Rdefinitions.v
@@ -8,17 +8,18 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-(* Classical quotient of the constructive Cauchy real numbers.
-   This file contains the definition of the classical real numbers
-   type R, its algebraic operations, its order and the proof that
-   it is total, and the proof that R is archimedean (up).
-   It also defines IZR, the ring morphism from Z to R. *)
+(* Abstraction of classical Dedekind reals behind an opaque module,
+   for backward compatibility.
+
+   This file also contains the proof that classical reals are a
+   quotient of constructive Cauchy reals. *)
 
 Require Export ZArith_base.
 Require Import QArith_base.
-Require Import ConstructiveRIneq.
+Require Import ConstructiveCauchyReals.
+Require Import ConstructiveCauchyRealsMult.
+Require Import ClassicalDedekindReals.
 
-Parameter R : Set.
 
 (* Declare primitive numeral notations for Scope R_scope *)
 Declare Scope R_scope.
@@ -27,26 +28,18 @@ Declare ML Module "r_syntax_plugin".
 (* Declare Scope R_scope with Key R *)
 Delimit Scope R_scope with R.
 
-(* Automatically open scope R_scope for arguments of type R *)
-Bind Scope R_scope with R.
-
 Local Open Scope R_scope.
 
-(* The limited principle of omniscience *)
-Axiom sig_forall_dec
-  : forall (P : nat -> Prop),
-    (forall n, {P n} + {~P n})
-    -> {n | ~P n} + {forall n, P n}.
-
-Axiom sig_not_dec : forall P : Prop, { ~~P } + { ~P }.
-
-Axiom Rabst : ConstructiveRIneq.R -> R.
-Axiom Rrepr : R -> ConstructiveRIneq.R.
-Axiom Rquot1 : forall x y:R, Req (Rrepr x) (Rrepr y) -> x = y.
-Axiom Rquot2 : forall x:ConstructiveRIneq.R, Req (Rrepr (Rabst x)) x.
 
 (* Those symbols must be kept opaque, for backward compatibility. *)
 Module Type RbaseSymbolsSig.
+  Parameter R : Set.
+  Bind Scope R_scope with R.
+  Axiom Rabst : CReal -> R.
+  Axiom Rrepr : R -> CReal.
+  Axiom Rquot1 : forall x y:R, CRealEq (Rrepr x) (Rrepr y) -> x = y.
+  Axiom Rquot2 : forall x:CReal, CRealEq (Rrepr (Rabst x)) x.
+
   Parameter R0 : R.
   Parameter R1 : R.
   Parameter Rplus : R -> R -> R.
@@ -54,29 +47,34 @@ Module Type RbaseSymbolsSig.
   Parameter Ropp : R -> R.
   Parameter Rlt : R -> R -> Prop.
 
-  Parameter R0_def : R0 = Rabst (CRzero CR).
-  Parameter R1_def : R1 = Rabst (CRone CR).
+  Parameter R0_def : R0 = Rabst (inject_Q 0).
+  Parameter R1_def : R1 = Rabst (inject_Q 1).
   Parameter Rplus_def : forall x y : R,
-      Rplus x y = Rabst (ConstructiveRIneq.Rplus (Rrepr x) (Rrepr y)).
+      Rplus x y = Rabst (CReal_plus (Rrepr x) (Rrepr y)).
   Parameter Rmult_def : forall x y : R,
-      Rmult x y = Rabst (ConstructiveRIneq.Rmult (Rrepr x) (Rrepr y)).
+      Rmult x y = Rabst (CReal_mult (Rrepr x) (Rrepr y)).
   Parameter Ropp_def : forall x : R,
-      Ropp x = Rabst (ConstructiveRIneq.Ropp (Rrepr x)).
+      Ropp x = Rabst (CReal_opp (Rrepr x)).
   Parameter Rlt_def : forall x y : R,
-      Rlt x y = ConstructiveRIneq.RltProp (Rrepr x) (Rrepr y).
+      Rlt x y = CRealLtProp (Rrepr x) (Rrepr y).
 End RbaseSymbolsSig.
 
 Module RbaseSymbolsImpl : RbaseSymbolsSig.
-  Definition R0 : R := Rabst (CRzero CR).
-  Definition R1 : R := Rabst (CRone CR).
+  Definition R := DReal.
+  Definition Rabst := DRealAbstr.
+  Definition Rrepr := DRealRepr.
+  Definition Rquot1 := DRealQuot1.
+  Definition Rquot2 := DRealQuot2.
+  Definition R0 : R := Rabst (inject_Q 0).
+  Definition R1 : R := Rabst (inject_Q 1).
   Definition Rplus : R -> R -> R
-    := fun x y : R => Rabst (ConstructiveRIneq.Rplus (Rrepr x) (Rrepr y)).
+    := fun x y : R => Rabst (CReal_plus (Rrepr x) (Rrepr y)).
   Definition Rmult : R -> R -> R
-    := fun x y : R => Rabst (ConstructiveRIneq.Rmult (Rrepr x) (Rrepr y)).
+    := fun x y : R => Rabst (CReal_mult (Rrepr x) (Rrepr y)).
   Definition Ropp : R -> R
-    := fun x : R => Rabst (ConstructiveRIneq.Ropp (Rrepr x)).
+    := fun x : R => Rabst (CReal_opp (Rrepr x)).
   Definition Rlt : R -> R -> Prop
-    := fun x y : R => ConstructiveRIneq.RltProp (Rrepr x) (Rrepr y).
+    := fun x y : R => CRealLtProp (Rrepr x) (Rrepr y).
 
   Definition R0_def := eq_refl R0.
   Definition R1_def := eq_refl R1.
@@ -88,6 +86,7 @@ End RbaseSymbolsImpl.
 Export RbaseSymbolsImpl.
 
 (* Keep the same names as before *)
+Notation R := RbaseSymbolsImpl.R (only parsing).
 Notation R0 := RbaseSymbolsImpl.R0 (only parsing).
 Notation R1 := RbaseSymbolsImpl.R1 (only parsing).
 Notation Rplus := RbaseSymbolsImpl.Rplus (only parsing).
@@ -95,6 +94,9 @@ Notation Rmult := RbaseSymbolsImpl.Rmult (only parsing).
 Notation Ropp := RbaseSymbolsImpl.Ropp (only parsing).
 Notation Rlt := RbaseSymbolsImpl.Rlt (only parsing).
 
+(* Automatically open scope R_scope for arguments of type R *)
+Bind Scope R_scope with R.
+
 Infix "+" := Rplus : R_scope.
 Infix "*" := Rmult : R_scope.
 Notation "- x" := (Ropp x) : R_scope.
@@ -160,11 +162,11 @@ Arguments IZR z%Z : simpl never.
 
 Lemma total_order_T : forall r1 r2:R, {Rlt r1 r2} + {r1 = r2} + {Rlt r2 r1}.
 Proof.
-  intros. destruct (Rlt_lpo_dec (Rrepr r1) (Rrepr r2) sig_forall_dec).
+  intros. destruct (CRealLt_lpo_dec (Rrepr r1) (Rrepr r2) sig_forall_dec).
   - left. left. rewrite RbaseSymbolsImpl.Rlt_def.
-    apply Rlt_forget. exact r.
-  - destruct (Rlt_lpo_dec (Rrepr r2) (Rrepr r1) sig_forall_dec).
-    + right. rewrite RbaseSymbolsImpl.Rlt_def. apply Rlt_forget. exact r0.
+    apply CRealLtForget. exact c.
+  - destruct (CRealLt_lpo_dec (Rrepr r2) (Rrepr r1) sig_forall_dec).
+    + right. rewrite RbaseSymbolsImpl.Rlt_def. apply CRealLtForget. exact c.
     + left. right. apply Rquot1. split; assumption.
 Qed.
 
@@ -178,9 +180,9 @@ Proof.
 Qed.
 
 Lemma Rrepr_appart_0 : forall x:R,
-    (x < R0 \/ R0 < x) -> Rappart (Rrepr x) (CRzero CR).
+    (x < R0 \/ R0 < x) -> CReal_appart (Rrepr x) (inject_Q 0).
 Proof.
-  intros. apply CRltDisjunctEpsilon. destruct H.
+  intros. apply CRealLtDisjunctEpsilon. destruct H.
   left. rewrite RbaseSymbolsImpl.Rlt_def, RbaseSymbolsImpl.R0_def, Rquot2 in H.
   exact H.
   right. rewrite RbaseSymbolsImpl.Rlt_def, RbaseSymbolsImpl.R0_def, Rquot2 in H.
@@ -192,7 +194,7 @@ Module Type RinvSig.
   Parameter Rinv_def : forall x : R,
       Rinv x = match Req_appart_dec x R0 with
                | left _ => R0 (* / 0 is undefined, we take 0 arbitrarily *)
-               | right r => Rabst ((ConstructiveRIneq.Rinv (Rrepr x) (Rrepr_appart_0 x r)))
+               | right r => Rabst ((CReal_inv (Rrepr x) (Rrepr_appart_0 x r)))
                end.
 End RinvSig.
 
@@ -200,7 +202,7 @@ Module RinvImpl : RinvSig.
   Definition Rinv : R -> R
     := fun x => match Req_appart_dec x R0 with
              | left _ => R0 (* / 0 is undefined, we take 0 arbitrarily *)
-             | right r => Rabst ((ConstructiveRIneq.Rinv (Rrepr x) (Rrepr_appart_0 x r)))
+             | right r => Rabst ((CReal_inv (Rrepr x) (Rrepr_appart_0 x r)))
              end.
   Definition Rinv_def := fun x => eq_refl (Rinv x).
 End RinvImpl.
@@ -215,7 +217,7 @@ Infix "/" := Rdiv   : R_scope.
 (* First integer strictly above x *)
 Definition up (x : R) : Z.
 Proof.
-  destruct (Rarchimedean (Rrepr x)) as [n nmaj], (total_order_T (IZR n - x) R1).
+  destruct (CRealArchimedean (Rrepr x)) as [n nmaj], (total_order_T (IZR n - x) R1).
   destruct s.
   - exact n.
   - (* x = n-1 *) exact n.