Use binary integers for Cauchy reals

5 files changed, 916 insertions, 1190 deletions

diff --git a/theories/Reals/Cauchy/ConstructiveCauchyAbs.v b/theories/Reals/Cauchy/ConstructiveCauchyAbs.v
index 7e51b575ba..ce263e1d21 100644
--- a/theories/Reals/Cauchy/ConstructiveCauchyAbs.v
+++ b/theories/Reals/Cauchy/ConstructiveCauchyAbs.v
@@ -31,9 +31,9 @@ Local Open Scope CReal_scope.
    uniquely extends to a uniformly continuous function
    CReal_abs : CReal -> CReal
 *)
-Lemma CauchyAbsStable : forall xn : nat -> Q,
-    QCauchySeq xn Pos.to_nat
-    -> QCauchySeq (fun n => Qabs (xn n)) Pos.to_nat.
+Lemma CauchyAbsStable : forall xn : positive -> Q,
+    QCauchySeq xn id
+    -> QCauchySeq (fun n => Qabs (xn n)) id.
 Proof.
   intros xn cau n p q H H0.
   specialize (cau n p q H H0).
@@ -53,23 +53,22 @@ Definition CReal_abs (x : CReal) : CReal
      exist _ (fun n => Qabs (xn n)) (CauchyAbsStable xn cau).
 
 Lemma CReal_neg_nth : forall (x : CReal) (n : positive),
-    (proj1_sig x (Pos.to_nat n) < -1#n)%Q
+    (proj1_sig x n < -1#n)%Q
     -> x < 0.
 Proof.
   intros. destruct x as [xn cau]; unfold proj1_sig in H.
   apply Qlt_minus_iff in H.
-  setoid_replace ((-1 # n) + - xn (Pos.to_nat n))%Q
-    with (- ((1 # n) + xn (Pos.to_nat n)))%Q in H.
-  destruct (Qarchimedean (2 / (-((1#n) + xn (Pos.to_nat n))))) as [k kmaj].
+  setoid_replace ((-1 # n) + - xn n)%Q
+    with (- ((1 # n) + xn n))%Q in H.
+  destruct (Qarchimedean (2 / (-((1#n) + xn n)))) as [k kmaj].
   exists (Pos.max k n). simpl. unfold Qminus; rewrite Qplus_0_l.
-  specialize (cau n (Pos.to_nat n) (max (Pos.to_nat k) (Pos.to_nat n))
-                  (le_refl _) (Nat.le_max_r _ _)).
+  specialize (cau n n (Pos.max k n)
+                  (Pos.le_refl _) (Pos.le_max_r _ _)).
   apply (Qle_lt_trans _ (2#k)).
   unfold Qle, Qnum, Qden.
   apply Z.mul_le_mono_nonneg_l. discriminate.
   apply Pos2Z.pos_le_pos, Pos.le_max_l.
-  rewrite <- Pos2Nat.inj_max in cau.
-  apply (Qmult_lt_l _ _ (-((1 # n) + xn (Pos.to_nat n)))) in kmaj.
+  apply (Qmult_lt_l _ _ (-((1 # n) + xn n))) in kmaj.
   rewrite Qmult_div_r in kmaj.
   apply (Qmult_lt_r _ _ (1 # k)) in kmaj.
   rewrite <- Qmult_assoc in kmaj.
@@ -77,13 +76,13 @@ Proof.
   rewrite Qmult_1_r in kmaj.
   setoid_replace (2#k)%Q with (2 * (1 # k))%Q. 2: reflexivity.
   apply (Qlt_trans _ _ _ kmaj). clear kmaj.
-  apply (Qplus_lt_l _ _ ((1#n) + xn (Pos.to_nat (Pos.max k n)))).
+  apply (Qplus_lt_l _ _ ((1#n) + xn (Pos.max k n))).
   ring_simplify. rewrite Qplus_comm.
-  apply (Qle_lt_trans _ (Qabs (xn (Pos.to_nat n) - xn (Pos.to_nat (Pos.max k n))))).
+  apply (Qle_lt_trans _ (Qabs (xn n - xn (Pos.max k n)))).
   2: exact cau.
   rewrite <- Qabs_opp.
-  setoid_replace (- (xn (Pos.to_nat n) - xn (Pos.to_nat (Pos.max k n))))%Q
-    with (xn (Pos.to_nat (Pos.max k n)) + -1 * xn (Pos.to_nat n))%Q.
+  setoid_replace (- (xn n - xn (Pos.max k n)))%Q
+    with (xn (Pos.max k n) + -1 * xn n)%Q.
   apply Qle_Qabs. ring. 2: reflexivity.
   unfold Qmult, Qeq, Qnum, Qden.
   rewrite Z.mul_1_r, Z.mul_1_r, Z.mul_1_l. reflexivity.
@@ -92,10 +91,10 @@ Proof.
 Qed.
 
 Lemma CReal_nonneg : forall (x : CReal) (n : positive),
-    0 <= x -> (-1#n <= proj1_sig x (Pos.to_nat n))%Q.
+    0 <= x -> (-1#n <= proj1_sig x n)%Q.
 Proof.
   intros. destruct x as [xn cau]; unfold proj1_sig.
-  destruct (Qlt_le_dec (xn (Pos.to_nat n)) (-1#n)).
+  destruct (Qlt_le_dec (xn n) (-1#n)).
   2: exact q. exfalso. apply H. clear H.
   apply (CReal_neg_nth _ n). exact q.
 Qed.
@@ -107,13 +106,13 @@ Proof.
   apply (CReal_nonneg _ n) in H. simpl in H.
   rewrite Qabs_pos.
   2: unfold Qminus; rewrite <- Qle_minus_iff; apply Qle_Qabs.
-  destruct (Qlt_le_dec (xn (Pos.to_nat n)) 0).
+  destruct (Qlt_le_dec (xn n) 0).
   - rewrite Qabs_neg. 2: apply Qlt_le_weak, q.
     apply Qopp_le_compat in H.
     apply (Qmult_le_l _ _ (1#2)). reflexivity. ring_simplify.
     setoid_replace ((1 # 2) * (2 # n))%Q with (-(-1#n))%Q.
     2: reflexivity.
-    setoid_replace ((-2 # 2) * xn (Pos.to_nat n))%Q with (- xn (Pos.to_nat n))%Q.
+    setoid_replace ((-2 # 2) * xn n)%Q with (- xn n)%Q.
     exact H. ring.
   - rewrite Qabs_pos. unfold Qminus. rewrite Qplus_opp_r. discriminate. exact q.
 Qed.
@@ -121,7 +120,7 @@ Qed.
 Lemma CReal_le_abs : forall x : CReal, x <= CReal_abs x.
 Proof.
   intros. intros [n nmaj]. destruct x as [xn cau]; simpl in nmaj.
-  apply (Qle_not_lt _ _ (Qle_Qabs (xn (Pos.to_nat n)))).
+  apply (Qle_not_lt _ _ (Qle_Qabs (xn n))).
   apply Qlt_minus_iff. apply (Qlt_trans _ (2#n)).
   reflexivity. exact nmaj.
 Qed.
@@ -129,7 +128,7 @@ Qed.
 Lemma CReal_abs_pos : forall x : CReal, 0 <= CReal_abs x.
 Proof.
   intros. intros [n nmaj]. destruct x as [xn cau]; simpl in nmaj.
-  apply (Qle_not_lt _ _ (Qabs_nonneg (xn (Pos.to_nat n)))).
+  apply (Qle_not_lt _ _ (Qabs_nonneg (xn n))).
   apply Qlt_minus_iff. apply (Qlt_trans _ (2#n)).
   reflexivity. exact nmaj.
 Qed.
@@ -153,7 +152,7 @@ Lemma CReal_abs_appart_0 : forall x : CReal,
     0 < CReal_abs x -> x # 0.
 Proof.
   intros x [n nmaj]. destruct x as [xn cau]; simpl in nmaj.
-  destruct (Qlt_le_dec (xn (Pos.to_nat n)) 0).
+  destruct (Qlt_le_dec (xn n) 0).
   - left. exists n. simpl. rewrite Qabs_neg in nmaj.
     apply (Qlt_le_trans _ _ _ nmaj). ring_simplify. apply Qle_refl.
     apply Qlt_le_weak, q.
@@ -189,7 +188,7 @@ Qed.
 Lemma CReal_abs_le : forall a b:CReal, -b <= a <= b -> CReal_abs a <= b.
 Proof.
   intros a b H [n nmaj]. destruct a as [an cau]; simpl in nmaj.
-  destruct (Qlt_le_dec (an (Pos.to_nat n)) 0).
+  destruct (Qlt_le_dec (an n) 0).
   - rewrite Qabs_neg in nmaj. destruct H. apply H. clear H H0.
     exists n. simpl.
     destruct b as [bn caub]; simpl; simpl in nmaj.
@@ -250,14 +249,14 @@ Lemma CReal_abs_gt : forall x : CReal,
     x < CReal_abs x -> x < 0.
 Proof.
   intros x [n nmaj]. destruct x as [xn cau]; simpl in nmaj.
-  assert (xn (Pos.to_nat n) < 0)%Q.
-  { destruct (Qlt_le_dec (xn (Pos.to_nat n)) 0). exact q.
+  assert (xn n < 0)%Q.
+  { destruct (Qlt_le_dec (xn n) 0). exact q.
     exfalso. rewrite Qabs_pos in nmaj. unfold Qminus in nmaj.
     rewrite Qplus_opp_r in nmaj. inversion nmaj. exact q. }
   rewrite Qabs_neg in nmaj. 2: apply Qlt_le_weak, H.
   apply (CReal_neg_nth _ n). simpl.
   ring_simplify in nmaj.
-  apply (Qplus_lt_l _ _ ((1#n) - xn (Pos.to_nat n))).
+  apply (Qplus_lt_l _ _ ((1#n) - xn n)).
   apply (Qmult_lt_l _ _ 2). reflexivity. ring_simplify.
   setoid_replace (2 * (1 # n))%Q with (2 # n)%Q. 2: reflexivity.
   rewrite <- Qplus_assoc.
@@ -274,7 +273,7 @@ Proof.
   destruct H as [i imaj]. destruct H0 as [j jmaj].
   exists (Pos.max i j). destruct x as [xn caux], y as [yn cauy]; simpl.
   simpl in imaj, jmaj.
-  destruct (Qlt_le_dec (xn (Pos.to_nat (Pos.max i j))) 0).
+  destruct (Qlt_le_dec (xn (Pos.max i j)) 0).
   - rewrite Qabs_neg.
     specialize (jmaj (Pos.max i j) (Pos.le_max_r _ _)).
     apply (Qle_lt_trans _ (2#j)). 2: exact jmaj.
diff --git a/theories/Reals/Cauchy/ConstructiveCauchyReals.v b/theories/Reals/Cauchy/ConstructiveCauchyReals.v
index 167f8d41c9..1a5335a573 100644
--- a/theories/Reals/Cauchy/ConstructiveCauchyReals.v
+++ b/theories/Reals/Cauchy/ConstructiveCauchyReals.v
@@ -33,20 +33,23 @@ Require CMorphisms.
     The double quantification on p q is needed to avoid
     forall un, QSeqEquiv un (fun _ => un O) (fun q => O)
     which says nothing about the limit of un.
+
+    We define sequences as positive -> Q instead of nat -> Q,
+    so that we can compute arguments like 2^n fast.
  *)
-Definition QSeqEquiv (un vn : nat -> Q) (cvmod : positive -> nat)
+Definition QSeqEquiv (un vn : positive -> Q) (cvmod : positive -> positive)
   : Prop
-  := forall (k : positive) (p q : nat),
-      le (cvmod k) p
-      -> le (cvmod k) q
+  := forall (k : positive) (p q : positive),
+      Pos.le (cvmod k) p
+      -> Pos.le (cvmod k) q
       -> Qlt (Qabs (un p - vn q)) (1 # k).
 
 (* A Cauchy sequence is a sequence equivalent to itself.
    If sequences are equivalent, they are both Cauchy and have the same limit. *)
-Definition QCauchySeq (un : nat -> Q) (cvmod : positive -> nat) : Prop
+Definition QCauchySeq (un : positive -> Q) (cvmod : positive -> positive) : Prop
   := QSeqEquiv un un cvmod.
 
-Lemma QSeqEquiv_sym : forall (un vn : nat -> Q) (cvmod : positive -> nat),
+Lemma QSeqEquiv_sym : forall (un vn : positive -> Q) (cvmod : positive -> positive),
     QSeqEquiv un vn cvmod
     -> QSeqEquiv vn un cvmod.
 Proof.
@@ -59,11 +62,12 @@ Proof.
   intros. unfold Qeq. simpl. destruct a; reflexivity.
 Qed.
 
-Lemma QSeqEquiv_trans : forall (un vn wn : nat -> Q)
-                          (cvmod cvmodw : positive -> nat),
+Lemma QSeqEquiv_trans : forall (un vn wn : positive -> Q)
+                          (cvmod cvmodw : positive -> positive),
     QSeqEquiv un vn cvmod
     -> QSeqEquiv vn wn cvmodw
-    -> QSeqEquiv un wn (fun q => max (cvmod (2 * q)%positive) (cvmodw (2 * q)%positive)).
+    -> QSeqEquiv un wn (fun q => Pos.max (cvmod (2 * q)%positive)
+                                     (cvmodw (2 * q)%positive)).
 Proof.
   intros. intros k p q H1 H2.
   setoid_replace (un p - wn q) with (un p - vn p + (vn p - wn q)).
@@ -71,38 +75,42 @@ Proof.
            _ (Qabs (un p - vn p) + Qabs (vn p - wn q))).
   apply Qabs_triangle. apply (Qlt_le_trans _ ((1 # (2*k)) + (1 # (2*k)))).
   apply Qplus_lt_le_compat.
-  - assert ((cvmod (2 * k)%positive <= p)%nat).
-    { apply (le_trans _ (max (cvmod (2 * k)%positive) (cvmodw (2 * k)%positive))).
-      apply Nat.le_max_l. assumption. }
+  - assert ((cvmod (2 * k)%positive <= p)%positive).
+    { apply (Pos.le_trans _ (Pos.max (cvmod (2 * k)%positive)
+                                     (cvmodw (2 * k)%positive))).
+      apply Pos.le_max_l. assumption. }
     apply H. assumption. assumption.
   - apply Qle_lteq. left. apply H0.
-    apply (le_trans _ (max (cvmod (2 * k)%positive) (cvmodw (2 * k)%positive))).
-    apply Nat.le_max_r. assumption.
-    apply (le_trans _ (max (cvmod (2 * k)%positive) (cvmodw (2 * k)%positive))).
-    apply Nat.le_max_r. assumption.
+    apply (Pos.le_trans _ (Pos.max (cvmod (2 * k)%positive)
+                                   (cvmodw (2 * k)%positive))).
+    apply Pos.le_max_r. assumption.
+    apply (Pos.le_trans _ (Pos.max (cvmod (2 * k)%positive)
+                                   (cvmodw (2 * k)%positive))).
+    apply Pos.le_max_r. assumption.
   - rewrite (factorDenom _ _ 2). ring_simplify. apply Qle_refl.
   - ring.
 Qed.
 
-Definition QSeqEquivEx (un vn : nat -> Q) : Prop
-  := exists (cvmod : positive -> nat), QSeqEquiv un vn cvmod.
+Definition QSeqEquivEx (un vn : positive -> Q) : Prop
+  := exists (cvmod : positive -> positive), QSeqEquiv un vn cvmod.
 
-Lemma QSeqEquivEx_sym : forall (un vn : nat -> Q), QSeqEquivEx un vn -> QSeqEquivEx vn un.
+Lemma QSeqEquivEx_sym : forall (un vn : positive -> Q),
+    QSeqEquivEx un vn -> QSeqEquivEx vn un.
 Proof.
   intros. destruct H. exists x. apply QSeqEquiv_sym. apply H.
 Qed.
 
-Lemma QSeqEquivEx_trans : forall un vn wn : nat -> Q,
+Lemma QSeqEquivEx_trans : forall un vn wn : positive -> Q,
     QSeqEquivEx un vn
     -> QSeqEquivEx vn wn
     -> QSeqEquivEx un wn.
 Proof.
   intros. destruct H,H0.
-  exists (fun q => max (x (2 * q)%positive) (x0 (2 * q)%positive)).
+  exists (fun q => Pos.max (x (2 * q)%positive) (x0 (2 * q)%positive)).
   apply (QSeqEquiv_trans un vn wn); assumption.
 Qed.
 
-Lemma QSeqEquiv_cau_r : forall (un vn : nat -> Q) (cvmod : positive -> nat),
+Lemma QSeqEquiv_cau_r : forall (un vn : positive -> Q) (cvmod : positive -> positive),
     QSeqEquiv un vn cvmod
     -> QCauchySeq vn (fun k => cvmod (2 * k)%positive).
 Proof.
@@ -118,82 +126,15 @@ Proof.
     apply Qabs_triangle.
     apply (Qlt_le_trans _ ((1 # (2 * k)) + (1 # (2 * k)))).
     apply Qplus_lt_le_compat.
-    + rewrite Qabs_Qminus. apply H. apply le_refl. assumption.
-    + apply Qle_lteq. left. apply H. apply le_refl. assumption.
+    + rewrite Qabs_Qminus. apply H. apply Pos.le_refl. assumption.
+    + apply Qle_lteq. left. apply H. apply Pos.le_refl. assumption.
     + rewrite (factorDenom _ _ 2). ring_simplify. apply Qle_refl.
   - ring.
 Qed.
 
-Fixpoint increasing_modulus (modulus : positive -> nat) (n : nat)
-  := match n with
-     | O => modulus xH
-     | S p => max (modulus (Pos.of_nat n)) (increasing_modulus modulus p)
-     end.
-
-Lemma increasing_modulus_inc : forall (modulus : positive -> nat) (n p : nat),
-    le (increasing_modulus modulus n)
-       (increasing_modulus modulus (p + n)).
-Proof.
-  induction p.
-  - apply le_refl.
-  - apply (le_trans _ (increasing_modulus modulus (p + n))).
-    apply IHp. simpl. destruct (plus p n). apply Nat.le_max_r. apply Nat.le_max_r.
-Qed.
-
-Lemma increasing_modulus_max : forall (modulus : positive -> nat) (p n : nat),
-    le n p -> le (modulus (Pos.of_nat n))
-                 (increasing_modulus modulus p).
-Proof.
-  induction p.
-  - intros. inversion H. subst n. apply le_refl.
-  - intros. simpl. destruct p. simpl.
-    + destruct n. apply Nat.le_max_l. apply le_S_n in H.
-      inversion H. apply Nat.le_max_l.
-    + apply Nat.le_succ_r in H. destruct H.
-      apply (le_trans _ (increasing_modulus modulus (S p))).
-      2: apply Nat.le_max_r. apply IHp. apply H.
-      subst n. apply (le_trans _ (modulus (Pos.succ (Pos.of_nat (S p))))).
-      apply le_refl. apply Nat.le_max_l.
-Qed.
-
-(* Choice of a standard element in each QSeqEquiv class. *)
-Lemma standard_modulus : forall (un : nat -> Q) (cvmod : positive -> nat),
-    QCauchySeq un cvmod
-    -> (QCauchySeq (fun n => un (increasing_modulus cvmod n)) Pos.to_nat
-       /\ QSeqEquiv un (fun n => un (increasing_modulus cvmod n))
-                   (fun p => max (cvmod p) (Pos.to_nat p))).
-Proof.
-  intros. split.
-  - intros k p q H0 H1. apply H.
-    + apply (le_trans _ (increasing_modulus cvmod (Pos.to_nat k))).
-      apply (le_trans _ (cvmod (Pos.of_nat (Pos.to_nat k)))).
-      rewrite Pos2Nat.id. apply le_refl.
-      destruct (Pos.to_nat k). apply le_refl. apply Nat.le_max_l.
-      destruct (Nat.le_exists_sub (Pos.to_nat k) p H0) as [i [H2 H3]]. subst p.
-      apply increasing_modulus_inc.
-    + apply (le_trans _ (increasing_modulus cvmod (Pos.to_nat k))).
-      apply (le_trans _ (cvmod (Pos.of_nat (Pos.to_nat k)))).
-      rewrite Pos2Nat.id. apply le_refl.
-      destruct (Pos.to_nat k). apply le_refl. apply Nat.le_max_l.
-      destruct (Nat.le_exists_sub (Pos.to_nat k) q H1) as [i [H2 H3]]. subst q.
-      apply increasing_modulus_inc.
-  - intros k p q H0 H1. apply H.
-    + apply (le_trans _ (Init.Nat.max (cvmod k) (Pos.to_nat k))).
-      apply Nat.le_max_l. assumption.
-    + apply (le_trans _ (increasing_modulus cvmod (Pos.to_nat k))).
-      apply (le_trans _ (cvmod (Pos.of_nat (Pos.to_nat k)))).
-      rewrite Pos2Nat.id. apply le_refl.
-      destruct (Pos.to_nat k). apply le_refl. apply Nat.le_max_l.
-      assert (le (Pos.to_nat k) q).
-      { apply (le_trans _ (Init.Nat.max (cvmod k) (Pos.to_nat k))).
-        apply Nat.le_max_r. assumption. }
-      destruct (Nat.le_exists_sub (Pos.to_nat k) q H2) as [i [H3 H4]]. subst q.
-      apply increasing_modulus_inc.
-Qed.
-
 (* A Cauchy real is a Cauchy sequence with the standard modulus *)
 Definition CReal : Set
-  := { x : (nat -> Q) | QCauchySeq x Pos.to_nat }.
+  := { x : (positive -> Q) | QCauchySeq x id }.
 
 Declare Scope CReal_scope.
 
@@ -208,12 +149,10 @@ Local Open Scope CReal_scope.
 
 (* So QSeqEquiv is the equivalence relation of this constructive pre-order *)
 Definition CRealLt (x y : CReal) : Set
-  := { n : positive |  Qlt (2 # n)
-                           (proj1_sig y (Pos.to_nat n) - proj1_sig x (Pos.to_nat n)) }.
+  := { n : positive |  Qlt (2 # n) (proj1_sig y n - proj1_sig x n) }.
 
 Definition CRealLtProp (x y : CReal) : Prop
-  := exists n : positive, Qlt (2 # n)
-                         (proj1_sig y (Pos.to_nat n) - proj1_sig x (Pos.to_nat n)).
+  := exists n : positive, Qlt (2 # n) (proj1_sig y n - proj1_sig x n).
 
 Definition CRealGt (x y : CReal) := CRealLt y x.
 Definition CReal_appart (x y : CReal) := sum (CRealLt x y) (CRealLt y x).
@@ -226,23 +165,23 @@ Infix "#" := CReal_appart : CReal_scope.
 Lemma CRealLtEpsilon : forall x y : CReal,
     CRealLtProp x y -> x < y.
 Proof.
-  intros.
-  assert (exists n : nat, n <> O
-                   /\ Qlt (2 # Pos.of_nat n) (proj1_sig y n - proj1_sig x n)).
-  { destruct H as [n maj]. exists (Pos.to_nat n). split.
-    intro abs. destruct (Pos2Nat.is_succ n). rewrite H in abs.
-    inversion abs. rewrite Pos2Nat.id. apply maj. }
+  intros. unfold CRealLtProp in H.
+  (* Convert to nat to use indefinite description. *)
+  assert (exists n : nat, lt O n /\ Qlt (2 # Pos.of_nat n)
+                                (proj1_sig y (Pos.of_nat n) - proj1_sig x (Pos.of_nat n))).
+  { destruct H as [n maj]. exists (Pos.to_nat n). split. apply Pos2Nat.is_pos.
+    rewrite Pos2Nat.id. exact maj. }
+  clear H.
   apply constructive_indefinite_ground_description_nat in H0.
-  destruct H0 as [n maj]. exists (Pos.of_nat n).
-  rewrite Nat2Pos.id. apply maj. apply maj.
+  destruct H0 as [n maj]. exists (Pos.of_nat n). exact (proj2 maj).
   intro n. destruct n. right.
-  intros [abs _]. exact (abs (eq_refl O)).
+  intros [abs _]. inversion abs.
   destruct (Qlt_le_dec (2 # Pos.of_nat (S n))
-                       (proj1_sig y (S n) - proj1_sig x (S n))).
-  left. split. discriminate. apply q.
+                       (proj1_sig y (Pos.of_nat (S n)) - proj1_sig x (Pos.of_nat (S n)))).
+  left. split. apply le_n_S, le_0_n. apply q.
   right. intros [_ abs].
   apply (Qlt_not_le (2 # Pos.of_nat (S n))
-                    (proj1_sig y (S n) - proj1_sig x (S n))); assumption.
+                    (proj1_sig y (Pos.of_nat (S n)) - proj1_sig x (Pos.of_nat (S n)))); assumption.
 Qed.
 
 Lemma CRealLtForget : forall x y : CReal,
@@ -254,18 +193,18 @@ Qed.
 (* CRealLt is decided by the LPO in Type,
    which is a non-constructive oracle. *)
 Lemma CRealLt_lpo_dec : forall x y : CReal,
-    (forall (P : nat -> Prop), (forall n, {P n} + {~P n})
+    (forall (P : nat -> Prop), (forall n:nat, {P n} + {~P n})
                     -> {n | ~P n} + {forall n, P n})
     -> CRealLt x y + (CRealLt x y -> False).
 Proof.
   intros x y lpo.
-  destruct (lpo (fun n:nat => Qle (proj1_sig y (S n) - proj1_sig x (S n))
+  destruct (lpo (fun n:nat => Qle (proj1_sig y (Pos.of_nat (S n)) - proj1_sig x (Pos.of_nat (S n)))
                              (2 # Pos.of_nat (S n)))).
   - intro n. destruct (Qlt_le_dec (2 # Pos.of_nat (S n))
-                                  (proj1_sig y (S n) - proj1_sig x (S n))).
+                                  (proj1_sig y (Pos.of_nat (S n)) - proj1_sig x (Pos.of_nat (S n)))).
     right. apply Qlt_not_le. exact q. left. exact q.
   - left. destruct s as [n nmaj]. exists (Pos.of_nat (S n)).
-    rewrite Nat2Pos.id. apply Qnot_le_lt. exact nmaj. discriminate.
+    apply Qnot_le_lt. exact nmaj.
   - right. intro abs. destruct abs as [n majn].
     specialize (q (pred (Pos.to_nat n))).
     replace (S (pred (Pos.to_nat n))) with (Pos.to_nat n) in q.
@@ -296,41 +235,37 @@ Definition CRealEq (x y : CReal) : Prop
 Infix "==" := CRealEq : CReal_scope.
 
 Lemma CRealLe_not_lt : forall x y : CReal,
-    (forall n:positive, Qle (proj1_sig x (Pos.to_nat n) - proj1_sig y (Pos.to_nat n))
-                       (2 # n))
+    (forall n:positive, Qle (proj1_sig x n - proj1_sig y n) (2 # n))
     <-> x <= y.
 Proof.
   intros. split.
   - intros. intro H0. destruct H0 as [n H0]. specialize (H n).
     apply (Qle_not_lt (2 # n) (2 # n)). apply Qle_refl.
-    apply (Qlt_le_trans _ (proj1_sig x (Pos.to_nat n) - proj1_sig y (Pos.to_nat n))).
+    apply (Qlt_le_trans _ (proj1_sig x n - proj1_sig y n)).
     assumption. assumption.
   - intros.
-    destruct (Qlt_le_dec (2 # n) (proj1_sig x (Pos.to_nat n) - proj1_sig y (Pos.to_nat n))).
+    destruct (Qlt_le_dec (2 # n) (proj1_sig x n - proj1_sig y n)).
     exfalso. apply H. exists n. assumption. assumption.
 Qed.
 
 Lemma CRealEq_diff : forall (x y : CReal),
     CRealEq x y
-    <-> forall n:positive, Qle (Qabs (proj1_sig x (Pos.to_nat n) - proj1_sig y (Pos.to_nat n)))
-                        (2 # n).
+    <-> forall n:positive, Qle (Qabs (proj1_sig x n - proj1_sig y n)) (2 # n).
 Proof.
   intros. split.
   - intros. destruct H. apply Qabs_case. intro.
     pose proof (CRealLe_not_lt x y) as [_ H2]. apply H2. assumption.
     intro. pose proof (CRealLe_not_lt y x) as [_ H2].
-    setoid_replace (- (proj1_sig x (Pos.to_nat n) - proj1_sig y (Pos.to_nat n)))
-      with (proj1_sig y (Pos.to_nat n) - proj1_sig x (Pos.to_nat n)).
+    setoid_replace (- (proj1_sig x n - proj1_sig y n))
+      with (proj1_sig y n - proj1_sig x n).
     apply H2. assumption. ring.
   - intros. split.
     + apply CRealLe_not_lt. intro n. specialize (H n).
       rewrite Qabs_Qminus in H.
-      apply (Qle_trans _ (Qabs (proj1_sig y (Pos.to_nat n)
-                                - proj1_sig x (Pos.to_nat n)))).
+      apply (Qle_trans _ (Qabs (proj1_sig y n - proj1_sig x n))).
       apply Qle_Qabs. apply H.
     + apply CRealLe_not_lt. intro n. specialize (H n).
-      apply (Qle_trans _ (Qabs (proj1_sig x (Pos.to_nat n)
-                                - proj1_sig y (Pos.to_nat n)))).
+      apply (Qle_trans _ (Qabs (proj1_sig x n - proj1_sig y n))).
       apply Qle_Qabs. apply H.
 Qed.
 
@@ -339,111 +274,106 @@ Qed.
 Lemma CRealEq_modindep : forall (x y : CReal),
     QSeqEquivEx (proj1_sig x) (proj1_sig y)
     <-> forall n:positive,
-      Qle (Qabs (proj1_sig x (Pos.to_nat n) - proj1_sig y (Pos.to_nat n))) (2 # n).
+      Qle (Qabs (proj1_sig x n - proj1_sig y n)) (2 # n).
 Proof.
   assert (forall x y: CReal, QSeqEquivEx (proj1_sig x) (proj1_sig y) -> x <= y ).
   { intros [xn limx] [yn limy] [cvmod H] [n abs]. simpl in abs, H.
-    pose (xn (Pos.to_nat n) - yn (Pos.to_nat n) - (2#n)) as eps.
+    pose (xn n - yn n - (2#n)) as eps.
     destruct (Qarchimedean (/eps)) as [k maj].
-    remember (max (cvmod k) (Pos.to_nat n)) as p.
-    assert (le (cvmod k) p).
-    { rewrite Heqp. apply Nat.le_max_l. }
-    assert (Pos.to_nat n <= p)%nat.
-    { rewrite Heqp. apply Nat.le_max_r. }
+    remember (Pos.max (cvmod k) n) as p.
+    assert (Pos.le (cvmod k) p).
+    { rewrite Heqp. apply Pos.le_max_l. }
+    assert (n <= p)%positive.
+    { rewrite Heqp. apply Pos.le_max_r. }
     specialize (H k p p H0 H0).
     setoid_replace (Z.pos k #1)%Q with (/ (1#k)) in maj. 2: reflexivity.
     apply Qinv_lt_contravar in maj. 2: reflexivity. unfold eps in maj.
     clear abs. (* less precise majoration *)
     apply (Qplus_lt_r _ _ (2#n)) in maj. ring_simplify in maj.
     apply (Qlt_not_le _ _ maj). clear maj.
-    setoid_replace (xn (Pos.to_nat n) + -1 * yn (Pos.to_nat n))
-      with (xn (Pos.to_nat n) - xn p + (xn p - yn p + (yn p - yn (Pos.to_nat n)))).
+    setoid_replace (xn n + -1 * yn n)
+      with (xn n - xn p + (xn p - yn p + (yn p - yn n))).
     2: ring.
     setoid_replace (2 # n)%Q with ((1 # n) + (1#n)).
     rewrite <- Qplus_assoc.
     apply Qplus_le_compat. apply (Qle_trans _ _ _ (Qle_Qabs _)).
-    apply Qlt_le_weak. apply limx. apply le_refl. assumption.
+    apply Qlt_le_weak. apply limx. apply Pos.le_refl. assumption.
     rewrite (Qplus_comm (1#n)).
     apply Qplus_le_compat. apply (Qle_trans _ _ _ (Qle_Qabs _)).
     apply Qlt_le_weak. exact H.
     apply (Qle_trans _ _ _ (Qle_Qabs _)). apply Qlt_le_weak. apply limy.
-    assumption. apply le_refl. ring_simplify. reflexivity.
+    assumption. apply Pos.le_refl. ring_simplify. reflexivity.
     unfold eps. unfold Qminus. rewrite <- Qlt_minus_iff. exact abs. }
   split.
   - rewrite <- CRealEq_diff. intros. split.
     apply H, QSeqEquivEx_sym. exact H0. apply H. exact H0.
   - clear H. intros. destruct x as [xn limx], y as [yn limy].
-    exists (fun q => Pos.to_nat (2 * (3 * q))). intros k p q H0 H1.
+    exists (fun q:positive => 2 * (3 * q))%positive. intros k p q H0 H1.
     unfold proj1_sig. specialize (H (2 * (3 * k))%positive).
-    assert ((Pos.to_nat (3 * k) <= Pos.to_nat (2 * (3 * k)))%nat).
-    { generalize (3 * k)%positive. intros. rewrite Pos2Nat.inj_mul.
-      rewrite <- (mult_1_l (Pos.to_nat p0)). apply Nat.mul_le_mono_nonneg.
-      auto. unfold Pos.to_nat. simpl. auto.
-      apply (le_trans 0 1). auto. apply Pos2Nat.is_pos. rewrite mult_1_l.
-      apply le_refl. }
+    assert (3 * k <= 2 * (3 * k))%positive.
+    { generalize (3 * k)%positive. intros. apply (Pos.le_trans _ (1 * p0)).
+      apply Pos.le_refl. rewrite <- Pos.mul_le_mono_r. discriminate. }
     setoid_replace (xn p - yn q)
-      with (xn p - xn (Pos.to_nat (2 * (3 * k)))
-            + (xn (Pos.to_nat (2 * (3 * k))) - yn (Pos.to_nat (2 * (3 * k)))
-               + (yn (Pos.to_nat (2 * (3 * k))) - yn q))).
+      with (xn p - xn (2 * (3 * k))%positive
+            + (xn (2 * (3 * k))%positive - yn (2 * (3 * k))%positive
+               + (yn (2 * (3 * k))%positive - yn q))).
+    2: ring.
     setoid_replace (1 # k)%Q with ((1 # 3 * k) + ((1 # 3 * k) + (1 # 3 * k))).
     apply (Qle_lt_trans
-             _ (Qabs (xn p - xn (Pos.to_nat (2 * (3 * k))))
-                + (Qabs (xn (Pos.to_nat (2 * (3 * k))) - yn (Pos.to_nat (2 * (3 * k)))
-                         + (yn (Pos.to_nat (2 * (3 * k))) - yn q))))).
+             _ (Qabs (xn p - xn (2 * (3 * k))%positive)
+                + (Qabs (xn (2 * (3 * k))%positive - yn (2 * (3 * k))%positive
+                         + (yn (2 * (3 * k))%positive - yn q))))).
     apply Qabs_triangle. apply Qplus_lt_le_compat.
-    apply limx. apply (le_trans _ (Pos.to_nat (2 * (3 * k)))). assumption. assumption.
+    apply limx. apply (Pos.le_trans _ (2 * (3 * k))). assumption. assumption.
     assumption.
     apply (Qle_trans
-             _ (Qabs (xn (Pos.to_nat (2 * (3 * k))) - yn (Pos.to_nat (2 * (3 * k))))
-                + Qabs (yn (Pos.to_nat (2 * (3 * k))) - yn q))).
+             _ (Qabs (xn (2 * (3 * k))%positive - yn (2 * (3 * k))%positive)
+                + Qabs (yn (2 * (3 * k))%positive - yn q))).
     apply Qabs_triangle. apply Qplus_le_compat.
     setoid_replace (1 # 3 * k)%Q with (2 # 2 * (3 * k))%Q. apply H.
-    rewrite (factorDenom _ _ 3). rewrite (factorDenom _ _ 2). rewrite (factorDenom _ _ 3).
+    rewrite (factorDenom _ _ 3).
+    rewrite (factorDenom _ _ 2). rewrite (factorDenom _ _ 3).
     rewrite Qmult_assoc. rewrite (Qmult_comm (1#2)).
     rewrite <- Qmult_assoc. apply Qmult_comp. reflexivity.
     unfold Qeq. reflexivity.
     apply Qle_lteq. left. apply limy. assumption.
-    apply (le_trans _ (Pos.to_nat (2 * (3 * k)))). assumption. assumption.
-    rewrite (factorDenom _ _ 3). ring_simplify. reflexivity. field.
+    apply (Pos.le_trans _ (2 * (3 * k))). assumption. assumption.
+    rewrite (factorDenom _ _ 3). ring_simplify. reflexivity.
 Qed.
 
 (* Extend separation to all indices above *)
 Lemma CRealLt_aboveSig : forall (x y : CReal) (n : positive),
     (Qlt (2 # n)
-         (proj1_sig y (Pos.to_nat n) - proj1_sig x (Pos.to_nat n)))
-    -> let (k, _) := Qarchimedean (/(proj1_sig y (Pos.to_nat n) - proj1_sig x (Pos.to_nat n) - (2#n)))
+         (proj1_sig y n - proj1_sig x n))
+    -> let (k, _) := Qarchimedean (/(proj1_sig y n - proj1_sig x n - (2#n)))
       in forall p:positive,
           Pos.le (Pos.max n (2*k)) p
           -> Qlt (2 # (Pos.max n (2*k)))
-                (proj1_sig y (Pos.to_nat p) - proj1_sig x (Pos.to_nat p)).
+                (proj1_sig y p - proj1_sig x p).
 Proof.
   intros [xn limx] [yn limy] n maj.
   unfold proj1_sig; unfold proj1_sig in maj.
-  pose (yn (Pos.to_nat n) - xn (Pos.to_nat n)) as dn.
-  destruct (Qarchimedean (/(yn (Pos.to_nat n) - xn (Pos.to_nat n) - (2#n)))) as [k kmaj].
-  assert (0 < yn (Pos.to_nat n) - xn (Pos.to_nat n) - (2 # n))%Q as H0.
+  pose (yn n - xn n) as dn.
+  destruct (Qarchimedean (/(yn n - xn n - (2#n)))) as [k kmaj].
+  assert (0 < yn n - xn n - (2 # n))%Q as H0.
   { rewrite <- (Qplus_opp_r (2#n)). apply Qplus_lt_l. assumption. }
-  intros.
-  remember (yn (Pos.to_nat p) - xn (Pos.to_nat p)) as dp.
-
+  intros. remember (yn p - xn p) as dp.
   rewrite <- (Qplus_0_r dp). rewrite <- (Qplus_opp_r dn).
   rewrite (Qplus_comm dn). rewrite Qplus_assoc.
   assert (Qlt (Qabs (dp - dn)) (2#n)).
   { rewrite Heqdp. unfold dn.
-    setoid_replace (yn (Pos.to_nat p) - xn (Pos.to_nat p) - (yn (Pos.to_nat n) - xn (Pos.to_nat n)))
-      with (yn (Pos.to_nat p) - yn (Pos.to_nat n)
-            + (xn (Pos.to_nat n) - xn (Pos.to_nat p))).
-    apply (Qle_lt_trans _ (Qabs (yn (Pos.to_nat p) - yn (Pos.to_nat n))
-                           + Qabs (xn (Pos.to_nat n) - xn (Pos.to_nat p)))).
+    setoid_replace (yn p - xn p - (yn n - xn n))
+      with (yn p - yn n + (xn n - xn p)).
+    apply (Qle_lt_trans _ (Qabs (yn p - yn n) + Qabs (xn n - xn p))).
     apply Qabs_triangle.
     setoid_replace (2#n)%Q with ((1#n) + (1#n))%Q.
     apply Qplus_lt_le_compat. apply limy.
-    apply Pos2Nat.inj_le. apply (Pos.le_trans _ (Pos.max n (2 * k))).
+    apply (Pos.le_trans _ (Pos.max n (2 * k))).
     apply Pos.le_max_l. assumption.
-    apply le_refl. apply Qlt_le_weak. apply limx. apply le_refl.
-    apply Pos2Nat.inj_le. apply (Pos.le_trans _ (Pos.max n (2 * k))).
+    apply Pos.le_refl. apply Qlt_le_weak. apply limx. apply Pos.le_refl.
+    apply (Pos.le_trans _ (Pos.max n (2 * k))).
     apply Pos.le_max_l. assumption.
-    rewrite Qinv_plus_distr. reflexivity. field. }
+    rewrite Qinv_plus_distr. reflexivity. ring. }
   apply (Qle_lt_trans _ (-(2#n) + dn)).
   rewrite Qplus_comm. unfold dn. apply Qlt_le_weak.
   apply (Qle_lt_trans _ (2 # (2 * k))). apply Pos.le_max_r.
@@ -463,12 +393,11 @@ Qed.
 Lemma CRealLt_above : forall (x y : CReal),
     CRealLt x y
     -> { k : positive | forall p:positive,
-          Pos.le k p -> Qlt (2 # k) (proj1_sig y (Pos.to_nat p)
-                                    - proj1_sig x (Pos.to_nat p)) }.
+          Pos.le k p -> Qlt (2 # k) (proj1_sig y p - proj1_sig x p) }.
 Proof.
   intros x y [n maj].
   pose proof (CRealLt_aboveSig x y n maj).
-  destruct (Qarchimedean (/ (proj1_sig y (Pos.to_nat n) - proj1_sig x (Pos.to_nat n) - (2 # n))))
+  destruct (Qarchimedean (/ (proj1_sig y n - proj1_sig x n - (2 # n))))
     as [k kmaj].
   exists (Pos.max n (2*k)). apply H.
 Qed.
@@ -476,28 +405,26 @@ Qed.
 (* The CRealLt index separates the Cauchy sequences *)
 Lemma CRealLt_above_same : forall (x y : CReal) (n : positive),
     Qlt (2 # n)
-        (proj1_sig y (Pos.to_nat n) - proj1_sig x (Pos.to_nat n))
-    -> forall p:positive, Pos.le n p
-                    -> Qlt (proj1_sig x (Pos.to_nat p)) (proj1_sig y (Pos.to_nat p)).
+        (proj1_sig y n - proj1_sig x n)
+    -> forall p:positive, Pos.le n p -> Qlt (proj1_sig x p) (proj1_sig y p).
 Proof.
   intros [xn limx] [yn limy] n inf p H.
   simpl. simpl in inf.
-  apply (Qplus_lt_l _ _ (- xn (Pos.to_nat n))).
-  apply (Qle_lt_trans _ (Qabs (xn (Pos.to_nat p) + - xn (Pos.to_nat n)))).
+  apply (Qplus_lt_l _ _ (- xn n)).
+  apply (Qle_lt_trans _ (Qabs (xn p + - xn n))).
   apply Qle_Qabs. apply (Qlt_trans _ (1#n)).
-  apply limx. apply Pos2Nat.inj_le. assumption. apply le_refl.
-  rewrite <- (Qplus_0_r (yn (Pos.to_nat p))).
-  rewrite <- (Qplus_opp_r (yn (Pos.to_nat n))).
-  rewrite (Qplus_comm (yn (Pos.to_nat n))). rewrite Qplus_assoc.
+  apply limx. exact H. apply Pos.le_refl.
+  rewrite <- (Qplus_0_r (yn p)).
+  rewrite <- (Qplus_opp_r (yn n)).
+  rewrite (Qplus_comm (yn n)). rewrite Qplus_assoc.
   rewrite <- Qplus_assoc.
   setoid_replace (1#n)%Q with (-(1#n) + (2#n))%Q. apply Qplus_lt_le_compat.
   apply (Qplus_lt_l _ _ (1#n)). rewrite Qplus_opp_r.
-  apply (Qplus_lt_r _ _ (yn (Pos.to_nat n) + - yn (Pos.to_nat p))).
+  apply (Qplus_lt_r _ _ (yn n + - yn p)).
   ring_simplify.
-  setoid_replace (yn (Pos.to_nat n) + (-1 # 1) * yn (Pos.to_nat p))
-    with (yn (Pos.to_nat n) - yn (Pos.to_nat p)).
-  apply (Qle_lt_trans _ (Qabs (yn (Pos.to_nat n) - yn (Pos.to_nat p)))).
-  apply Qle_Qabs. apply limy. apply le_refl. apply Pos2Nat.inj_le. assumption.
+  setoid_replace (yn n + (-1 # 1) * yn p) with (yn n - yn p).
+  apply (Qle_lt_trans _ (Qabs (yn n - yn p))).
+  apply Qle_Qabs. apply limy. apply Pos.le_refl. assumption.
   field. apply Qle_lteq. left. assumption.
   rewrite Qplus_comm. rewrite Qinv_minus_distr.
   reflexivity.
@@ -508,10 +435,10 @@ Proof.
   intros x y H [n q].
   apply CRealLt_above in H. destruct H as [p H].
   pose proof (CRealLt_above_same y x n q).
-  apply (Qlt_not_le (proj1_sig y (Pos.to_nat (Pos.max n p)))
-                    (proj1_sig x (Pos.to_nat (Pos.max n p)))).
+  apply (Qlt_not_le (proj1_sig y (Pos.max n p))
+                    (proj1_sig x (Pos.max n p))).
   apply H0. apply Pos.le_max_l.
-  apply Qlt_le_weak. apply (Qplus_lt_l _ _ (-proj1_sig x (Pos.to_nat (Pos.max n p)))).
+  apply Qlt_le_weak. apply (Qplus_lt_l _ _ (-proj1_sig x (Pos.max n p))).
   rewrite Qplus_opp_r. apply (Qlt_trans _ (2#p)).
   unfold Qlt. simpl. unfold Z.lt. auto. apply H. apply Pos.le_max_r.
 Qed.
@@ -542,31 +469,24 @@ Lemma CRealLt_dec : forall x y z : CReal,
 Proof.
   intros [xn limx] [yn limy] [zn limz] [n inf].
   unfold proj1_sig in inf.
-  remember (yn (Pos.to_nat n) - xn (Pos.to_nat n) - (2 # n)) as eps.
+  remember (yn n - xn n - (2 # n)) as eps.
   assert (Qlt 0 eps) as epsPos.
   { subst eps. unfold Qminus. apply (Qlt_minus_iff (2#n)). assumption. }
-  assert (forall n p, Pos.to_nat n <= Pos.to_nat (Pos.max n p))%nat.
-  { intros. apply Pos2Nat.inj_le. unfold Pos.max. unfold Pos.le.
-    destruct (n0 ?= p)%positive eqn:des.
-    rewrite des. discriminate. rewrite des. discriminate.
-    unfold Pos.compare. rewrite Pos.compare_cont_refl. discriminate. }
   destruct (Qarchimedean (/eps)) as [k kmaj].
-  destruct (Qlt_le_dec ((yn (Pos.to_nat n) + xn (Pos.to_nat n)) / (2#1))
-                       (zn (Pos.to_nat (Pos.max n (4 * k)))))
+  destruct (Qlt_le_dec ((yn n + xn n) / (2#1))
+                       (zn (Pos.max n (4 * k))))
     as [decMiddle|decMiddle].
   - left. exists (Pos.max n (4 * k)). unfold proj1_sig. unfold Qminus.
-    rewrite <- (Qplus_0_r (zn (Pos.to_nat (Pos.max n (4 * k))))).
-    rewrite <- (Qplus_opp_r (xn (Pos.to_nat n))).
-    rewrite (Qplus_comm (xn (Pos.to_nat n))). rewrite Qplus_assoc.
+    rewrite <- (Qplus_0_r (zn (Pos.max n (4 * k)))).
+    rewrite <- (Qplus_opp_r (xn n)).
+    rewrite (Qplus_comm (xn n)). rewrite Qplus_assoc.
     rewrite <- Qplus_assoc. rewrite <- Qplus_0_r.
     rewrite <- (Qplus_opp_r (1#n)). rewrite Qplus_assoc.
     apply Qplus_lt_le_compat.
-    + apply (Qplus_lt_l _ _ (- xn (Pos.to_nat n))) in decMiddle.
-      apply (Qlt_trans _ ((yn (Pos.to_nat n) + xn (Pos.to_nat n)) / (2 # 1)
-                          + - xn (Pos.to_nat n))).
-      setoid_replace ((yn (Pos.to_nat n) + xn (Pos.to_nat n)) / (2 # 1)
-                      - xn (Pos.to_nat n))
-        with ((yn (Pos.to_nat n) - xn (Pos.to_nat n)) / (2 # 1)).
+    + apply (Qplus_lt_l _ _ (- xn n)) in decMiddle.
+      apply (Qlt_trans _ ((yn n + xn n) / (2 # 1) + - xn n)).
+      setoid_replace ((yn n + xn n) / (2 # 1) - xn n)
+        with ((yn n - xn n) / (2 # 1)).
       apply Qlt_shift_div_l. unfold Qlt. simpl. unfold Z.lt. auto.
       rewrite Qmult_plus_distr_l.
       setoid_replace ((1 # n) * (2 # 1))%Q with (2#n)%Q.
@@ -580,31 +500,30 @@ Proof.
       apply Qinv_lt_contravar. reflexivity. apply epsPos. apply kmaj.
       unfold Qeq. simpl. rewrite Pos.mul_1_r. reflexivity.
       field. assumption.
-    + setoid_replace (xn (Pos.to_nat n) + - xn (Pos.to_nat (Pos.max n (4 * k))))
-        with (-(xn (Pos.to_nat (Pos.max n (4 * k))) - xn (Pos.to_nat n))).
+    + setoid_replace (xn n + - xn (Pos.max n (4 * k)))
+        with (-(xn (Pos.max n (4 * k)) - xn n)).
       apply Qopp_le_compat.
-      apply (Qle_trans _ (Qabs (xn (Pos.to_nat (Pos.max n (4 * k))) - xn (Pos.to_nat n)))).
-      apply Qle_Qabs. apply Qle_lteq. left. apply limx. apply H.
-      apply le_refl. field.
+      apply (Qle_trans _ (Qabs (xn (Pos.max n (4 * k)) - xn n))).
+      apply Qle_Qabs. apply Qle_lteq. left. apply limx. apply Pos.le_max_l.
+      apply Pos.le_refl. ring.
   - right. exists (Pos.max n (4 * k)). unfold proj1_sig. unfold Qminus.
-    rewrite <- (Qplus_0_r (yn (Pos.to_nat (Pos.max n (4 * k))))).
-    rewrite <- (Qplus_opp_r (yn (Pos.to_nat n))).
-    rewrite (Qplus_comm (yn (Pos.to_nat n))). rewrite Qplus_assoc.
+    rewrite <- (Qplus_0_r (yn (Pos.max n (4 * k)))).
+    rewrite <- (Qplus_opp_r (yn n)).
+    rewrite (Qplus_comm (yn n)). rewrite Qplus_assoc.
     rewrite <- Qplus_assoc. rewrite <- Qplus_0_l.
     rewrite <- (Qplus_opp_r (1#n)). rewrite (Qplus_comm (1#n)).
     rewrite <- Qplus_assoc. apply Qplus_lt_le_compat.
-    + apply (Qplus_lt_r _ _ (yn (Pos.to_nat n) - yn (Pos.to_nat (Pos.max n (4 * k))) + (1#n)))
+    + apply (Qplus_lt_r _ _ (yn n - yn (Pos.max n (4 * k)) + (1#n)))
       ; ring_simplify.
-      setoid_replace (-1 * yn (Pos.to_nat (Pos.max n (4 * k))))
-        with (- yn (Pos.to_nat (Pos.max n (4 * k)))). 2: ring.
-      apply (Qle_lt_trans _ (Qabs (yn (Pos.to_nat n)
-                                   - yn (Pos.to_nat (Pos.max n (4 * k)))))).
-      apply Qle_Qabs. apply limy. apply le_refl. apply H.
+      setoid_replace (-1 * yn (Pos.max n (4 * k)))
+        with (- yn (Pos.max n (4 * k))). 2: ring.
+      apply (Qle_lt_trans _ (Qabs (yn n - yn (Pos.max n (4 * k))))).
+      apply Qle_Qabs. apply limy. apply Pos.le_refl. apply Pos.le_max_l.
     + apply Qopp_le_compat in decMiddle.
-      apply (Qplus_le_r _ _ (yn (Pos.to_nat n))) in decMiddle.
-      apply (Qle_trans _ (yn (Pos.to_nat n) + - ((yn (Pos.to_nat n) + xn (Pos.to_nat n)) / (2 # 1)))).
-      setoid_replace (yn (Pos.to_nat n) + - ((yn (Pos.to_nat n) + xn (Pos.to_nat n)) / (2 # 1)))
-        with ((yn (Pos.to_nat n) - xn (Pos.to_nat n)) / (2 # 1)).
+      apply (Qplus_le_r _ _ (yn n)) in decMiddle.
+      apply (Qle_trans _ (yn n + - ((yn n + xn n) / (2 # 1)))).
+      setoid_replace (yn n + - ((yn n + xn n) / (2 # 1)))
+        with ((yn n - xn n) / (2 # 1)).
       apply Qle_shift_div_l. unfold Qlt. simpl. unfold Z.lt. auto.
       rewrite Qmult_plus_distr_l.
       setoid_replace ((1 # n) * (2 # 1))%Q with (2#n)%Q.
@@ -766,7 +685,7 @@ Qed.
 (* Injection of Q into CReal *)
 
 Lemma ConstCauchy : forall q : Q,
-    QCauchySeq (fun _ => q) Pos.to_nat.
+    QCauchySeq (fun _ => q) id.
 Proof.
   intros. intros k p r H H0.
   unfold Qminus. rewrite Qplus_opp_r. unfold Qlt. simpl.
@@ -811,64 +730,64 @@ Qed.
    by a factor 2. *)
 Lemma CRealLtQ : forall (x : CReal) (q : Q),
     CRealLt x (inject_Q q)
-    -> forall p:positive, Qlt (proj1_sig x (Pos.to_nat p)) (q + (1#p)).
+    -> forall p:positive, Qlt (proj1_sig x p) (q + (1#p)).
 Proof.
   intros [xn cau] q maj p. simpl.
-  destruct (Qlt_le_dec (xn (Pos.to_nat p)) (q + (1 # p))). assumption.
+  destruct (Qlt_le_dec (xn p) (q + (1 # p))). assumption.
   exfalso.
   apply CRealLt_above in maj.
   destruct maj as [k maj]; simpl in maj.
   specialize (maj (Pos.max k p) (Pos.le_max_l _ _)).
-  specialize (cau p (Pos.to_nat p) (Pos.to_nat (Pos.max k p)) (le_refl _)).
-  pose proof (Qplus_lt_le_compat (2#k) (q - xn (Pos.to_nat (Pos.max k p)))
-                                 (q + (1 # p)) (xn (Pos.to_nat p)) maj q0).
+  specialize (cau p p (Pos.max k p) (Pos.le_refl _)).
+  pose proof (Qplus_lt_le_compat (2#k) (q - xn (Pos.max k p))
+                                 (q + (1 # p)) (xn p) maj q0).
   rewrite Qplus_comm in H. unfold Qminus in H. rewrite <- Qplus_assoc in H.
   rewrite <- Qplus_assoc in H. apply Qplus_lt_r in H.
-  rewrite <- (Qplus_lt_r _ _ (xn (Pos.to_nat p))) in maj.
+  rewrite <- (Qplus_lt_r _ _ (xn p)) in maj.
   apply (Qlt_not_le (1#p) ((1 # p) + (2 # k))).
   rewrite <- (Qplus_0_r (1#p)). rewrite <- Qplus_assoc.
   apply Qplus_lt_r. reflexivity.
   apply Qlt_le_weak.
-  apply (Qlt_trans _ (- xn (Pos.to_nat (Pos.max k p)) + xn (Pos.to_nat p)) _ H).
+  apply (Qlt_trans _ (- xn (Pos.max k p) + xn p) _ H).
   rewrite Qplus_comm.
-  apply (Qle_lt_trans _ (Qabs (xn (Pos.to_nat p) - xn (Pos.to_nat (Pos.max k p))))).
-  apply Qle_Qabs. apply cau. apply Pos2Nat.inj_le. apply Pos.le_max_r.
+  apply (Qle_lt_trans _ (Qabs (xn p - xn (Pos.max k p)))).
+  apply Qle_Qabs. apply cau. apply Pos.le_max_r.
 Qed.
 
 Lemma CRealLtQopp : forall (x : CReal) (q : Q),
     CRealLt (inject_Q q) x
-    -> forall p:positive, Qlt (q - (1#p)) (proj1_sig x (Pos.to_nat p)).
+    -> forall p:positive, Qlt (q - (1#p)) (proj1_sig x p).
 Proof.
   intros [xn cau] q maj p. simpl.
-  destruct (Qlt_le_dec (q - (1 # p)) (xn (Pos.to_nat p))). assumption.
+  destruct (Qlt_le_dec (q - (1 # p)) (xn p)). assumption.
   exfalso.
   apply CRealLt_above in maj.
   destruct maj as [k maj]; simpl in maj.
   specialize (maj (Pos.max k p) (Pos.le_max_l _ _)).
-  specialize (cau p (Pos.to_nat (Pos.max k p)) (Pos.to_nat p)).
-  pose proof (Qplus_lt_le_compat (2#k) (xn (Pos.to_nat (Pos.max k p)) - q)
-                                 (xn (Pos.to_nat p)) (q - (1 # p)) maj q0).
+  specialize (cau p (Pos.max k p) p).
+  pose proof (Qplus_lt_le_compat (2#k) (xn (Pos.max k p) - q)
+                                 (xn p) (q - (1 # p)) maj q0).
   unfold Qminus in H. rewrite <- Qplus_assoc in H.
   rewrite (Qplus_assoc (-q)) in H. rewrite (Qplus_comm (-q)) in H.
   rewrite Qplus_opp_r in H. rewrite Qplus_0_l in H.
   apply (Qplus_lt_l _ _ (1#p)) in H.
-  rewrite <- (Qplus_assoc (xn (Pos.to_nat (Pos.max k p)))) in H.
+  rewrite <- (Qplus_assoc (xn (Pos.max k p))) in H.
   rewrite (Qplus_comm (-(1#p))) in H. rewrite Qplus_opp_r in H.
   rewrite Qplus_0_r in H. rewrite Qplus_comm in H.
-  rewrite Qplus_assoc in H. apply (Qplus_lt_l _ _ (- xn (Pos.to_nat p))) in H.
+  rewrite Qplus_assoc in H. apply (Qplus_lt_l _ _ (- xn p)) in H.
   rewrite <- Qplus_assoc in H. rewrite Qplus_opp_r in H. rewrite Qplus_0_r in H.
   apply (Qlt_not_le (1#p) ((1 # p) + (2 # k))).
   rewrite <- (Qplus_0_r (1#p)). rewrite <- Qplus_assoc.
   apply Qplus_lt_r. reflexivity.
   apply Qlt_le_weak.
-  apply (Qlt_trans _ (xn (Pos.to_nat (Pos.max k p)) - xn (Pos.to_nat p)) _ H).
-  apply (Qle_lt_trans _ (Qabs (xn (Pos.to_nat (Pos.max k p)) - xn (Pos.to_nat p)))).
-  apply Qle_Qabs. apply cau. apply Pos2Nat.inj_le.
-  apply Pos.le_max_r. apply le_refl.
+  apply (Qlt_trans _ (xn (Pos.max k p) - xn p) _ H).
+  apply (Qle_lt_trans _ (Qabs (xn (Pos.max k p) - xn p))).
+  apply Qle_Qabs. apply cau.
+  apply Pos.le_max_r. apply Pos.le_refl.
 Qed.
 
 Lemma inject_Q_compare : forall (x : CReal) (p : positive),
-    x <= inject_Q (proj1_sig x (Pos.to_nat p) + (1#p)).
+    x <= inject_Q (proj1_sig x p + (1#p)).
 Proof.
   intros. intros [n nmaj].
   destruct x as [xn xcau]; simpl in nmaj.
@@ -876,18 +795,17 @@ Proof.
   ring_simplify in nmaj.
   destruct (Pos.max_dec p n).
   - apply Pos.max_l_iff in e.
-    apply Pos2Nat.inj_le in e.
-    specialize (xcau n (Pos.to_nat n) (Pos.to_nat p) (le_refl _) e).
-    apply (Qlt_le_trans _ _ (Qabs (xn (Pos.to_nat n) + -1 * xn (Pos.to_nat p)))) in nmaj.
+    specialize (xcau n n p (Pos.le_refl _) e).
+    apply (Qlt_le_trans _ _ (Qabs (xn n + -1 * xn p))) in nmaj.
     2: apply Qle_Qabs.
     apply (Qlt_trans _ _ _ nmaj) in xcau.
     apply (Qplus_lt_l _ _ (-(1#n)-(1#p))) in xcau. ring_simplify in xcau.
     setoid_replace ((2 # n) + -1 * (1 # n)) with (1#n)%Q in xcau.
     discriminate xcau. setoid_replace (-1 * (1 # n)) with (-1#n)%Q. 2: reflexivity.
     rewrite Qinv_plus_distr. reflexivity.
-  - apply Pos.max_r_iff, Pos2Nat.inj_le in e.
-    specialize (xcau p (Pos.to_nat n) (Pos.to_nat p) e (le_refl _)).
-    apply (Qlt_le_trans _ _ (Qabs (xn (Pos.to_nat n) + -1 * xn (Pos.to_nat p)))) in nmaj.
+  - apply Pos.max_r_iff in e.
+    specialize (xcau p n p e (Pos.le_refl _)).
+    apply (Qlt_le_trans _ _ (Qabs (xn n + -1 * xn p))) in nmaj.
     2: apply Qle_Qabs.
     apply (Qlt_trans _ _ _ nmaj) in xcau.
     apply (Qplus_lt_l _ _ (-(1#p))) in xcau. ring_simplify in xcau. discriminate.
@@ -921,12 +839,12 @@ Qed.
 (* Algebraic operations *)
 
 Lemma CReal_plus_cauchy
-  : forall (xn yn zn : nat -> Q) (cvmod : positive -> nat),
+  : forall (xn yn zn : positive -> Q) (cvmod : positive -> positive),
     QSeqEquiv xn yn cvmod
-    -> QCauchySeq zn Pos.to_nat
-    -> QSeqEquiv (fun n:nat => xn n + zn n) (fun n:nat => yn n + zn n)
-                (fun p => max (cvmod (2 * p)%positive)
-                           (Pos.to_nat (2 * p)%positive)).
+    -> QCauchySeq zn id
+    -> QSeqEquiv (fun n:positive => xn n + zn n) (fun n:positive => yn n + zn n)
+                (fun p => Pos.max (cvmod (2 * p)%positive)
+                               (2 * p)%positive).
 Proof.
   intros. intros p n k H1 H2.
   setoid_replace (xn n + zn n - (yn k + zn k))
@@ -936,70 +854,67 @@ Proof.
   apply Qabs_triangle.
   setoid_replace (1#p)%Q with ((1#2*p) + (1#2*p))%Q.
   apply Qplus_lt_le_compat.
-  - apply H. apply (le_trans _ (Init.Nat.max (cvmod (2 * p)%positive) (Pos.to_nat (2 * p)))).
-    apply Nat.le_max_l. apply H1.
-    apply (le_trans _ (Init.Nat.max (cvmod (2 * p)%positive) (Pos.to_nat (2 * p)))).
-    apply Nat.le_max_l. apply H2.
+  - apply H. apply (Pos.le_trans _ (Pos.max (cvmod (2 * p)%positive) (2 * p))).
+    apply Pos.le_max_l. apply H1.
+    apply (Pos.le_trans _ (Pos.max (cvmod (2 * p)%positive) (2 * p))).
+    apply Pos.le_max_l. apply H2.
   - apply Qle_lteq. left. apply H0.
-    apply (le_trans _ (Init.Nat.max (cvmod (2 * p)%positive) (Pos.to_nat (2 * p)))).
-    apply Nat.le_max_r. apply H1.
-    apply (le_trans _ (Init.Nat.max (cvmod (2 * p)%positive) (Pos.to_nat (2 * p)))).
-    apply Nat.le_max_r. apply H2.
+    apply (Pos.le_trans _ (Pos.max (cvmod (2 * p)%positive) (2 * p))).
+    apply Pos.le_max_r. apply H1.
+    apply (Pos.le_trans _ (Pos.max (cvmod (2 * p)%positive) (2 * p))).
+    apply Pos.le_max_r. apply H2.
   - rewrite Qinv_plus_distr. unfold Qeq. reflexivity.
 Qed.
 
 Definition CReal_plus (x y : CReal) : CReal.
 Proof.
   destruct x as [xn limx], y as [yn limy].
-  pose proof (CReal_plus_cauchy xn xn yn Pos.to_nat limx limy).
-  exists (fun n : nat => xn (2 * n)%nat + yn (2 * n)%nat).
+  pose proof (CReal_plus_cauchy xn xn yn id limx limy).
+  exists (fun n : positive => xn (2 * n)%positive + yn (2 * n)%positive).
   intros p k n H0 H1. apply H.
-  - rewrite max_l. rewrite Pos2Nat.inj_mul.
-    apply Nat.mul_le_mono_nonneg. apply le_0_n. apply le_refl.
-    apply le_0_n. apply H0. apply le_refl.
-  - rewrite Pos2Nat.inj_mul. rewrite max_l.
-    apply Nat.mul_le_mono_nonneg. apply le_0_n. apply le_refl.
-    apply le_0_n. apply H1. apply le_refl.
+  - rewrite Pos.max_l. unfold id. rewrite <- Pos.mul_le_mono_l.
+    exact H0. apply Pos.le_refl.
+  - rewrite Pos.max_l. unfold id.
+    apply Pos.mul_le_mono_l. exact H1. apply Pos.le_refl.
 Defined.
 
 Infix "+" := CReal_plus : CReal_scope.
 
-Lemma CReal_plus_nth : forall (x y : CReal) (n : nat),
-    proj1_sig (x + y) n = Qplus (proj1_sig x (2*n)%nat) (proj1_sig y (2*n)%nat).
+Lemma CReal_plus_nth : forall (x y : CReal) (n : positive),
+    proj1_sig (x + y) n = Qplus (proj1_sig x (2*n)%positive)
+                                (proj1_sig y (2*n)%positive).
 Proof.
   intros. destruct x,y; reflexivity.
 Qed.
 
 Lemma CReal_plus_unfold : forall (x y : CReal),
     QSeqEquiv (proj1_sig (CReal_plus x y))
-              (fun n : nat => proj1_sig x n + proj1_sig y n)%Q
-              (fun p => Pos.to_nat (2 * p)).
+              (fun n : positive => proj1_sig x n + proj1_sig y n)%Q
+              (fun p => 2 * p)%positive.
 Proof.
   intros [xn limx] [yn limy].
   unfold CReal_plus; simpl.
   intros p n k H H0.
-  setoid_replace (xn (2 * n)%nat + yn (2 * n)%nat - (xn k + yn k))%Q
-    with (xn (2 * n)%nat - xn k + (yn (2 * n)%nat - yn k))%Q.
+  setoid_replace (xn (2 * n)%positive + yn (2 * n)%positive - (xn k + yn k))%Q
+    with (xn (2 * n)%positive - xn k + (yn (2 * n)%positive - yn k))%Q.
   2: field.
-  apply (Qle_lt_trans _ (Qabs (xn (2 * n)%nat - xn k) + Qabs (yn (2 * n)%nat - yn k))).
+  apply (Qle_lt_trans _ (Qabs (xn (2 * n)%positive - xn k) + Qabs (yn (2 * n)%positive - yn k))).
   apply Qabs_triangle.
   setoid_replace (1#p)%Q with ((1#2*p) + (1#2*p))%Q.
   apply Qplus_lt_le_compat.
-  - apply limx. apply (le_trans _ n). apply H.
-    rewrite <- (mult_1_l n). rewrite mult_assoc.
-    apply Nat.mul_le_mono_nonneg. auto. simpl. auto.
-    apply le_0_n. apply le_refl. apply H0.
-  - apply Qlt_le_weak. apply limy. apply (le_trans _ n). apply H.
-    rewrite <- (mult_1_l n). rewrite mult_assoc.
-    apply Nat.mul_le_mono_nonneg. auto. simpl. auto.
-    apply le_0_n. apply le_refl. apply H0.
+  - apply limx. apply (Pos.le_trans _ n). apply H.
+    apply (Pos.le_trans _ (1 * n)). apply Pos.le_refl.
+    apply Pos.mul_le_mono_r. discriminate. exact H0.
+  - apply Qlt_le_weak. apply limy. apply (Pos.le_trans _ n). apply H.
+    apply (Pos.le_trans _ (1 * n)). apply Pos.le_refl.
+    apply Pos.mul_le_mono_r. discriminate. exact H0.
   - rewrite Qinv_plus_distr. unfold Qeq. reflexivity.
 Qed.
 
 Definition CReal_opp (x : CReal) : CReal.
 Proof.
   destruct x as [xn limx].
-  exists (fun n : nat => - xn n).
+  exists (fun n : positive => - xn n).
   intros k p q H H0. unfold Qminus. rewrite Qopp_involutive.
   rewrite Qplus_comm. apply limx; assumption.
 Defined.
@@ -1011,10 +926,10 @@ Definition CReal_minus (x y : CReal) : CReal
 
 Infix "-" := CReal_minus : CReal_scope.
 
-Lemma belowMultiple : forall n p : nat, lt 0 p -> le n (p * n).
+Lemma belowMultiple : forall n p : positive, Pos.le n (p * n).
 Proof.
-  intros. rewrite <- (mult_1_l n). apply Nat.mul_le_mono_nonneg.
-  auto. assumption. apply le_0_n. rewrite mult_1_l. apply le_refl.
+  intros. apply (Pos.le_trans _ (1*n)). apply Pos.le_refl.
+  apply Pos.mul_le_mono_r. destruct p; discriminate.
 Qed.
 
 Lemma CReal_plus_assoc : forall (x y z : CReal),
@@ -1024,20 +939,20 @@ Proof.
   intros. apply CRealEq_diff. intro n.
   destruct x as [xn limx], y as [yn limy], z as [zn limz].
   unfold CReal_plus; unfold proj1_sig.
-  setoid_replace (xn (2 * (2 * Pos.to_nat n))%nat + yn (2 * (2 * Pos.to_nat n))%nat
-                  + zn (2 * Pos.to_nat n)%nat
-                    - (xn (2 * Pos.to_nat n)%nat + (yn (2 * (2 * Pos.to_nat n))%nat
-                                                    + zn (2 * (2 * Pos.to_nat n))%nat)))%Q
-    with (xn (2 * (2 * Pos.to_nat n))%nat - xn (2 * Pos.to_nat n)%nat
-          + (zn (2 * Pos.to_nat n)%nat - zn (2 * (2 * Pos.to_nat n))%nat))%Q.
-  apply (Qle_trans _ (Qabs (xn (2 * (2 * Pos.to_nat n))%nat - xn (2 * Pos.to_nat n)%nat)
-                      + Qabs (zn (2 * Pos.to_nat n)%nat - zn (2 * (2 * Pos.to_nat n))%nat))).
+  setoid_replace (xn (2 * (2 * n))%positive + yn (2 * (2 * n))%positive
+                  + zn (2 * n)%positive
+                    - (xn (2 * n)%positive + (yn (2 * (2 * n))%positive
+                                                    + zn (2 * (2 * n))%positive)))%Q
+    with (xn (2 * (2 * n))%positive - xn (2 * n)%positive
+          + (zn (2 * n)%positive - zn (2 * (2 * n))%positive))%Q.
+  apply (Qle_trans _ (Qabs (xn (2 * (2 * n))%positive - xn (2 * n)%positive)
+                      + Qabs (zn (2 * n)%positive - zn (2 * (2 * n))%positive))).
   apply Qabs_triangle.
   rewrite <- (Qinv_plus_distr 1 1 n). apply Qplus_le_compat.
-  apply Qle_lteq. left. apply limx. rewrite mult_assoc.
-  apply belowMultiple. simpl. auto. apply belowMultiple. auto.
-  apply Qle_lteq. left. apply limz. apply belowMultiple. auto.
-  rewrite mult_assoc. apply belowMultiple. simpl. auto. field.
+  apply Qle_lteq. left. apply limx. rewrite Pos.mul_assoc.
+  apply belowMultiple. apply belowMultiple.
+  apply Qle_lteq. left. apply limz. apply belowMultiple.
+  rewrite Pos.mul_assoc. apply belowMultiple. simpl. field.
 Qed.
 
 Lemma CReal_plus_comm : forall x y : CReal,
@@ -1045,39 +960,40 @@ Lemma CReal_plus_comm : forall x y : CReal,
 Proof.
   intros [xn limx] [yn limy]. apply CRealEq_diff. intros.
   unfold CReal_plus, proj1_sig.
-  setoid_replace (xn (2 * Pos.to_nat n)%nat + yn (2 * Pos.to_nat n)%nat
-                    - (yn (2 * Pos.to_nat n)%nat + xn (2 * Pos.to_nat n)%nat))%Q
+  setoid_replace (xn (2 * n)%positive + yn (2 * n)%positive
+                    - (yn (2 * n)%positive + xn (2 * n)%positive))%Q
     with 0%Q.
   unfold Qle. simpl. unfold Z.le. intro absurd. inversion absurd.
   field.
 Qed.
 
 Lemma CReal_plus_0_l : forall r : CReal,
-    CRealEq (CReal_plus (inject_Q 0) r) r.
+    inject_Q 0 + r == r.
 Proof.
-  intro r. assert (forall n:nat, le n (2 * n)).
-  { intro n. simpl. rewrite <- (plus_0_r n). rewrite <- plus_assoc.
-    apply Nat.add_le_mono_l. apply le_0_n. }
-  split.
-  - intros [n maj]. destruct r as [xn q]; unfold CReal_plus, proj1_sig, inject_Q in maj.
+  intro r. split.
+  - intros [n maj].
+    destruct r as [xn q]; unfold CReal_plus, proj1_sig, inject_Q in maj.
     rewrite Qplus_0_l in maj.
-    specialize (q n (Pos.to_nat n) (mult 2 (Pos.to_nat n)) (le_refl _)).
-    apply (Qlt_not_le (2#n) (xn (Pos.to_nat n) - xn (2 * Pos.to_nat n)%nat)).
+    specialize (q n n (Pos.mul 2 n) (Pos.le_refl _)).
+    apply (Qlt_not_le (2#n) (xn n - xn (2 * n)%positive)).
     assumption.
-    apply (Qle_trans _ (Qabs (xn (Pos.to_nat n) - xn (2 * Pos.to_nat n)%nat))).
+    apply (Qle_trans _ (Qabs (xn n - xn (2 * n)%positive))).
     apply Qle_Qabs. apply (Qle_trans _ (1#n)). apply Qlt_le_weak. apply q.
-    apply H. unfold Qle, Z.le; simpl. apply Pos2Nat.inj_le. rewrite Pos2Nat.inj_xO.
-    apply H.
-  - intros [n maj]. destruct r as [xn q]; unfold CReal_plus, proj1_sig, inject_Q in maj.
+    apply belowMultiple.
+    unfold Qle, Qnum, Qden. apply Z.mul_le_mono_nonneg_r.
+    discriminate. discriminate.
+  - intros [n maj].
+    destruct r as [xn q]; unfold CReal_plus, proj1_sig, inject_Q in maj.
     rewrite Qplus_0_l in maj.
-    specialize (q n (Pos.to_nat n) (mult 2 (Pos.to_nat n)) (le_refl _)).
+    specialize (q n n (Pos.mul 2 n) (Pos.le_refl _)).
     rewrite Qabs_Qminus in q.
-    apply (Qlt_not_le (2#n) (xn (mult 2 (Pos.to_nat n)) - xn (Pos.to_nat n))).
+    apply (Qlt_not_le (2#n) (xn (Pos.mul 2 n) - xn n)).
     assumption.
-    apply (Qle_trans _ (Qabs (xn (mult 2 (Pos.to_nat n)) - xn (Pos.to_nat n)))).
+    apply (Qle_trans _ (Qabs (xn (Pos.mul 2 n) - xn n))).
     apply Qle_Qabs. apply (Qle_trans _ (1#n)). apply Qlt_le_weak. apply q.
-    apply H. unfold Qle, Z.le; simpl. apply Pos2Nat.inj_le. rewrite Pos2Nat.inj_xO.
-    apply H.
+    apply belowMultiple.
+    unfold Qle, Qnum, Qden. apply Z.mul_le_mono_nonneg_r.
+    discriminate. discriminate.
 Qed.
 
 Lemma CReal_plus_0_r : forall r : CReal,
@@ -1091,14 +1007,11 @@ Lemma CReal_plus_lt_compat_l :
 Proof.
   intros.
   apply CRealLt_above in H. destruct H as [n maj].
-  exists n. specialize (maj (xO n)).
-  rewrite Pos2Nat.inj_xO in maj.
-  setoid_replace (proj1_sig (CReal_plus x z) (Pos.to_nat n)
-                  - proj1_sig (CReal_plus x y) (Pos.to_nat n))%Q
-    with (proj1_sig z (2 * Pos.to_nat n)%nat - proj1_sig y (2 * Pos.to_nat n)%nat)%Q.
-  apply maj. apply Pos2Nat.inj_le.
-  rewrite <- (plus_0_r (Pos.to_nat n)). rewrite Pos2Nat.inj_xO.
-  simpl. apply Nat.add_le_mono_l. apply le_0_n.
+  exists n. specialize (maj (2 * n)%positive).
+  setoid_replace (proj1_sig (CReal_plus x z) n
+                  - proj1_sig (CReal_plus x y) n)%Q
+    with (proj1_sig z (2 * n)%positive - proj1_sig y (2 * n)%positive)%Q.
+  apply maj. apply belowMultiple.
   simpl. destruct x as [xn limx], y as [yn limy], z as [zn limz].
   simpl; ring.
 Qed.
@@ -1114,12 +1027,13 @@ Lemma CReal_plus_lt_reg_l :
   forall x y z : CReal, x + y < x + z -> y < z.
 Proof.
   intros. destruct H as [n maj]. exists (2*n)%positive.
-  setoid_replace (proj1_sig z (Pos.to_nat (2 * n)) - proj1_sig y (Pos.to_nat (2 * n)))%Q
-      with (proj1_sig (CReal_plus x z) (Pos.to_nat n) - proj1_sig (CReal_plus x y) (Pos.to_nat n))%Q.
-  apply (Qle_lt_trans _ (2#n)). unfold Qle, Z.le; simpl. apply Pos2Nat.inj_le.
-  rewrite <- (plus_0_r (Pos.to_nat n~0)). rewrite (Pos2Nat.inj_xO (n~0)).
-  simpl. apply Nat.add_le_mono_l. apply le_0_n.
-  apply maj. rewrite Pos2Nat.inj_xO.
+  setoid_replace (proj1_sig z (2 * n)%positive - proj1_sig y (2 * n)%positive)%Q
+      with (proj1_sig (CReal_plus x z) n - proj1_sig (CReal_plus x y) n)%Q.
+  apply (Qle_lt_trans _ (2#n)).
+  setoid_replace (2 # 2 * n)%Q with (1 # n)%Q. 2: reflexivity.
+  unfold Qle, Qnum, Qden. apply Z.mul_le_mono_nonneg_r.
+  discriminate. discriminate.
+  apply maj.
   destruct x as [xn limx], y as [yn limy], z as [zn limz].
   simpl; ring.
 Qed.
@@ -1173,7 +1087,7 @@ Lemma CReal_plus_opp_r : forall x : CReal,
 Proof.
   intros [xn limx]. apply CRealEq_diff. intros.
   unfold CReal_plus, CReal_opp, inject_Q, proj1_sig.
-  setoid_replace (xn (2 * Pos.to_nat n)%nat + - xn (2 * Pos.to_nat n)%nat - 0)%Q
+  setoid_replace (xn (2 * n)%positive + - xn (2 * n)%positive - 0)%Q
     with 0%Q.
   unfold Qle. simpl. unfold Z.le. intro absurd. inversion absurd. field.
 Qed.
diff --git a/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v b/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v
index fc57fc4056..f3a59b493f 100644
--- a/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v
+++ b/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v
@@ -20,7 +20,7 @@ Require CMorphisms.
 
 Local Open Scope CReal_scope.
 
-Definition QCauchySeq_bound (qn : nat -> Q) (cvmod : positive -> nat)
+Definition QCauchySeq_bound (qn : positive -> Q) (cvmod : positive -> positive)
   : positive
   := match Qnum (qn (cvmod 1%positive)) with
      | Z0 => 1%positive
@@ -28,13 +28,13 @@ Definition QCauchySeq_bound (qn : nat -> Q) (cvmod : positive -> nat)
      | Z.neg p => p + 1
      end.
 
-Lemma QCauchySeq_bounded_prop (qn : nat -> Q) (cvmod : positive -> nat)
+Lemma QCauchySeq_bounded_prop (qn : positive -> Q) (cvmod : positive -> positive)
   : QCauchySeq qn cvmod
-    -> forall n:nat, le (cvmod 1%positive) n
-             -> Qlt (Qabs (qn n)) (Z.pos (QCauchySeq_bound qn cvmod) # 1).
+    -> forall n:positive, Pos.le (cvmod 1%positive) n
+                    -> Qlt (Qabs (qn n)) (Z.pos (QCauchySeq_bound qn cvmod) # 1).
 Proof.
   intros H n H0. unfold QCauchySeq_bound.
-  specialize (H 1%positive (cvmod 1%positive) n (le_refl _) H0).
+  specialize (H 1%positive (cvmod 1%positive) n (Pos.le_refl _) H0).
   destruct (qn (cvmod 1%positive)) as [a b]. unfold Qnum.
   rewrite Qabs_Qminus in H.
   apply (Qplus_lt_l _ _ (-Qabs (a#b))).
@@ -56,24 +56,21 @@ Proof.
 Qed.
 
 Lemma CReal_mult_cauchy
-  : forall (xn yn zn : nat -> Q) (Ay Az : positive) (cvmod : positive -> nat),
+  : forall (xn yn zn : positive -> Q) (Ay Az : positive) (cvmod : positive -> positive),
     QSeqEquiv xn yn cvmod
-    -> QCauchySeq zn Pos.to_nat
-    -> (forall n:nat, le (cvmod 2%positive) n
+    -> QCauchySeq zn id
+    -> (forall n:positive, Pos.le (cvmod 2%positive) n
               -> Qlt (Qabs (yn n)) (Z.pos Ay # 1))
-    -> (forall n:nat, le 1 n
+    -> (forall n:positive, Pos.le 1 n
               -> Qlt (Qabs (zn n)) (Z.pos Az # 1))
-    -> QSeqEquiv (fun n:nat => xn n * zn n) (fun n:nat => yn n * zn n)
-                (fun p => max (max (cvmod 2%positive)
+    -> QSeqEquiv (fun n:positive => xn n * zn n) (fun n:positive => yn n * zn n)
+                (fun p => Pos.max (Pos.max (cvmod 2%positive)
                                 (cvmod (2 * (Pos.max Ay Az) * p)%positive))
-                           (Pos.to_nat (2 * (Pos.max Ay Az) * p)%positive)).
+                               (2 * (Pos.max Ay Az) * p)%positive).
 Proof.
   intros xn yn zn Ay Az cvmod limx limz majy majz.
   remember (Pos.mul 2 (Pos.max Ay Az)) as z.
   intros k p q H H0.
-  assert (Pos.to_nat k <> O) as kPos.
-  { intro absurd. pose proof (Pos2Nat.is_pos k).
-    rewrite absurd in H1. inversion H1. }
   setoid_replace (xn p * zn p - yn q * zn q)%Q
     with ((xn p - yn q) * zn p + yn q * (zn p - zn q))%Q.
   2: ring.
@@ -84,12 +81,12 @@ Proof.
   apply Qplus_lt_le_compat.
   - apply (Qle_lt_trans _ ((1#z * k) * Qabs (zn p)%nat)).
     + apply Qmult_le_compat_r. apply Qle_lteq. left. apply limx.
-      apply (le_trans _ (Init.Nat.max (cvmod (z * k)%positive) (Pos.to_nat (z * k)))).
-      apply Nat.le_max_l. refine (le_trans _ _ _ _ H).
-      rewrite <- Nat.max_assoc. apply Nat.le_max_r.
-      apply (le_trans _ (Init.Nat.max (cvmod (z * k)%positive) (Pos.to_nat (z * k)))).
-      apply Nat.le_max_l. refine (le_trans _ _ _ _ H0).
-      rewrite <- Nat.max_assoc. apply Nat.le_max_r. apply Qabs_nonneg.
+      apply (Pos.le_trans _ (Pos.max (cvmod (z * k)%positive) (z * k))).
+      apply Pos.le_max_l. refine (Pos.le_trans _ _ _ _ H).
+      rewrite <- Pos.max_assoc. apply Pos.le_max_r.
+      apply (Pos.le_trans _ (Pos.max (cvmod (z * k)%positive) (z * k))).
+      apply Pos.le_max_l. refine (Pos.le_trans _ _ _ _ H0).
+      rewrite <- Pos.max_assoc. apply Pos.le_max_r. apply Qabs_nonneg.
     + subst z. rewrite <- (Qmult_1_r (1 # 2 * k)).
       rewrite <- Pos.mul_assoc. rewrite <- (Pos.mul_comm k). rewrite Pos.mul_assoc.
       rewrite (factorDenom _ _ (2 * k)). rewrite <- Qmult_assoc.
@@ -102,21 +99,20 @@ Proof.
       rewrite Qmult_comm. apply Qmult_lt_l. reflexivity.
       setoid_replace (/(1#Az))%Q with (Z.pos Az # 1)%Q.
       2: reflexivity.
-      apply majz.
-      refine (le_trans _ _ _ _ H).
-      apply (le_trans _ (Pos.to_nat (2 * Pos.max Ay Az * k))).
-      apply Pos2Nat.is_pos. apply Nat.le_max_r.
+      apply majz. refine (Pos.le_trans _ _ _ _ H).
+      apply (Pos.le_trans _ (2 * Pos.max Ay Az * k)).
+      discriminate. apply Pos.le_max_r.
   - apply (Qle_trans _ ((1 # z * k) * Qabs (yn q)%nat)).
     + rewrite Qmult_comm. apply Qmult_le_compat_r. apply Qle_lteq.
       left. apply limz.
-      apply (le_trans _ (max (cvmod (z * k)%positive)
-                             (Pos.to_nat (z * k)%positive))).
-      apply Nat.le_max_r. refine (le_trans _ _ _ _ H).
-      rewrite <- Nat.max_assoc. apply Nat.le_max_r.
-      apply (le_trans _ (max (cvmod (z * k)%positive)
-                             (Pos.to_nat (z * k)%positive))).
-      apply Nat.le_max_r. refine (le_trans _ _ _ _ H0).
-      rewrite <- Nat.max_assoc. apply Nat.le_max_r.
+      apply (Pos.le_trans _ (Pos.max (cvmod (z * k)%positive)
+                             (z * k)%positive)).
+      apply Pos.le_max_r. refine (Pos.le_trans _ _ _ _ H).
+      rewrite <- Pos.max_assoc. apply Pos.le_max_r.
+      apply (Pos.le_trans _ (Pos.max (cvmod (z * k)%positive)
+                             (z * k)%positive)).
+      apply Pos.le_max_r. refine (Pos.le_trans _ _ _ _ H0).
+      rewrite <- Pos.max_assoc. apply Pos.le_max_r.
       apply Qabs_nonneg.
     + subst z. rewrite <- (Qmult_1_r (1 # 2 * k)).
       rewrite <- Pos.mul_assoc. rewrite <- (Pos.mul_comm k). rewrite Pos.mul_assoc.
@@ -130,38 +126,36 @@ Proof.
       2: intro abs; inversion abs.
       rewrite Qmult_comm. apply Qmult_lt_l. reflexivity.
       setoid_replace (/(1#Ay))%Q with (Z.pos Ay # 1)%Q. 2: reflexivity.
-      apply majy. refine (le_trans _ _ _ _ H0).
-      rewrite <- Nat.max_assoc. apply Nat.le_max_l.
+      apply majy. refine (Pos.le_trans _ _ _ _ H0).
+      rewrite <- Pos.max_assoc. apply Pos.le_max_l.
   - rewrite Qinv_plus_distr. unfold Qeq. reflexivity.
 Qed.
 
-Lemma linear_max : forall (p Ax Ay : positive) (i : nat),
-  le (Pos.to_nat p) i
-  -> (max (max 2 (Pos.to_nat (2 * Pos.max Ax Ay * p)))
-         (Pos.to_nat (2 * Pos.max Ax Ay * p))
-     <= Pos.to_nat (2 * Pos.max Ax Ay) * i)%nat.
-Proof.
-  intros. rewrite max_l. 2: apply Nat.le_max_r. rewrite max_r.
-  rewrite Pos2Nat.inj_mul. apply Nat.mul_le_mono_nonneg.
-  apply le_0_n. apply le_refl. apply le_0_n. exact H.
-  apply (Pos2Nat.inj_le 2). rewrite <- Pos.mul_assoc.
-  apply (Pos.mul_le_mono_l 2 1).
-  rewrite <- (Pos.mul_le_mono_l 2 1).
+Lemma linear_max : forall (p Ax Ay i : positive),
+  Pos.le p i
+  -> (Pos.max (Pos.max 2 (2 * Pos.max Ax Ay * p))
+         (2 * Pos.max Ax Ay * p)
+     <= (2 * Pos.max Ax Ay) * i)%positive.
+Proof.
+  intros. rewrite Pos.max_l. 2: apply Pos.le_max_r. rewrite Pos.max_r.
+  apply Pos.mul_le_mono_l. exact H.
+  apply (Pos.le_trans _ (2*1)). apply Pos.le_refl.
+  rewrite <- Pos.mul_assoc, <- (Pos.mul_le_mono_l 2).
   destruct (Pos.max Ax Ay * p)%positive; discriminate.
 Qed.
 
 Definition CReal_mult (x y : CReal) : CReal.
 Proof.
   destruct x as [xn limx]. destruct y as [yn limy].
-  pose (QCauchySeq_bound xn Pos.to_nat) as Ax.
-  pose (QCauchySeq_bound yn Pos.to_nat) as Ay.
-  exists (fun n : nat => xn (Pos.to_nat (2 * Pos.max Ax Ay) * n)%nat
-               * yn (Pos.to_nat (2 * Pos.max Ax Ay) * n)%nat).
+  pose (QCauchySeq_bound xn id) as Ax.
+  pose (QCauchySeq_bound yn id) as Ay.
+  exists (fun n : positive => xn ((2 * Pos.max Ax Ay) * n)%positive
+               * yn ((2 * Pos.max Ax Ay) * n)%positive).
   intros p n k H0 H1.
-  apply (CReal_mult_cauchy xn xn yn Ax Ay Pos.to_nat limx limy).
-  intros. apply (QCauchySeq_bounded_prop xn Pos.to_nat limx).
-  apply (le_trans _ (Pos.to_nat 2)). apply le_S, le_refl. exact H.
-  intros. exact (QCauchySeq_bounded_prop yn Pos.to_nat limy _ H).
+  apply (CReal_mult_cauchy xn xn yn Ax Ay id limx limy).
+  intros. apply (QCauchySeq_bounded_prop xn id limx).
+  apply (Pos.le_trans _ 2). discriminate. exact H.
+  intros. exact (QCauchySeq_bounded_prop yn id limy _ H).
   apply linear_max; assumption. apply linear_max; assumption.
 Defined.
 
@@ -169,45 +163,44 @@ Infix "*" := CReal_mult : CReal_scope.
 
 Lemma CReal_mult_unfold : forall x y : CReal,
     QSeqEquivEx (proj1_sig (CReal_mult x y))
-                (fun n : nat => proj1_sig x n * proj1_sig y n)%Q.
+                (fun n : positive => proj1_sig x n * proj1_sig y n)%Q.
 Proof.
   intros [xn limx] [yn limy]. unfold CReal_mult ; simpl.
-  pose proof (QCauchySeq_bounded_prop xn Pos.to_nat limx) as majx.
-  pose proof (QCauchySeq_bounded_prop yn Pos.to_nat limy) as majy.
-  remember (QCauchySeq_bound xn Pos.to_nat) as Ax.
-  remember (QCauchySeq_bound yn Pos.to_nat) as Ay.
+  pose proof (QCauchySeq_bounded_prop xn id limx) as majx.
+  pose proof (QCauchySeq_bounded_prop yn id limy) as majy.
+  remember (QCauchySeq_bound xn id) as Ax.
+  remember (QCauchySeq_bound yn id) as Ay.
   exists (fun p : positive =>
-         Init.Nat.max (Pos.to_nat (2 * Pos.max Ax Ay * p))
-           (Pos.to_nat (2 * Pos.max Ax Ay * p))).
-  intros p n k H0 H1. rewrite max_l in H0, H1.
-  apply (CReal_mult_cauchy xn xn yn Ax Ay Pos.to_nat limx limy).
+         Pos.max (2 * Pos.max Ax Ay * p)
+           (2 * Pos.max Ax Ay * p)).
+  intros p n k H0 H1. rewrite Pos.max_l in H0, H1.
+  apply (CReal_mult_cauchy xn xn yn Ax Ay id limx limy).
   2: apply majy. intros. apply majx.
-  refine (le_trans _ _ _ _ H). apply le_S, le_refl.
-  3: apply le_refl. 3: apply le_refl.
-  apply linear_max. refine (le_trans _ _ _ _ H0).
-  rewrite <- (mult_1_l (Pos.to_nat p)). rewrite Pos2Nat.inj_mul.
-  apply Nat.mul_le_mono_nonneg. auto. apply Pos2Nat.is_pos.
-  apply le_0_n. apply le_refl. rewrite max_l.
-  rewrite Nat.max_r. apply H1. apply Pos2Nat.inj_le.
-  2: apply Nat.le_max_r.
-  apply (Pos.le_trans _ (2*1)). apply Pos.le_refl.
+  refine (Pos.le_trans _ _ _ _ H). discriminate.
+  3: apply Pos.le_refl. 3: apply Pos.le_refl.
+  apply linear_max. refine (Pos.le_trans _ _ _ _ H0).
+  apply (Pos.le_trans _ (1*p)). apply Pos.le_refl.
+  apply Pos.mul_le_mono_r. discriminate.
+  rewrite Pos.max_l.
+  rewrite Pos.max_r. apply H1. 2: apply Pos.le_max_r.
+  apply (Pos.le_trans _ (2*1)). apply Pos.le_refl. unfold id.
   rewrite <- Pos.mul_assoc, <- (Pos.mul_le_mono_l 2 1).
   destruct (Pos.max Ax Ay * p)%positive; discriminate.
 Qed.
 
-Lemma CReal_mult_assoc_bounded_r : forall (xn yn zn : nat -> Q),
+Lemma CReal_mult_assoc_bounded_r : forall (xn yn zn : positive -> Q),
     QSeqEquivEx xn yn (* both are Cauchy with same limit *)
-    -> QSeqEquiv zn zn Pos.to_nat
+    -> QSeqEquiv zn zn id
     -> QSeqEquivEx (fun n => xn n * zn n)%Q (fun n => yn n * zn n)%Q.
 Proof.
   intros xn yn zn [cvmod cveq] H0.
-  exists (fun p => max (max (cvmod 2%positive) (cvmod (2 * (Pos.max (QCauchySeq_bound yn (fun k : positive => cvmod (2 * k)%positive)) (QCauchySeq_bound zn Pos.to_nat)) * p)%positive))
-               (Pos.to_nat (2 * (Pos.max (QCauchySeq_bound yn (fun k : positive => cvmod (2 * k)%positive)) (QCauchySeq_bound zn Pos.to_nat)) * p)%positive)).
+  exists (fun p => Pos.max (Pos.max (cvmod 2%positive) (cvmod (2 * (Pos.max (QCauchySeq_bound yn (fun k : positive => cvmod (2 * k)%positive)) (QCauchySeq_bound zn id)) * p)%positive))
+               (2 * (Pos.max (QCauchySeq_bound yn (fun k : positive => cvmod (2 * k)%positive)) (QCauchySeq_bound zn id)) * p)%positive).
   apply (CReal_mult_cauchy _ _ _ _ _ _ cveq H0).
   exact (QCauchySeq_bounded_prop
            yn (fun k => cvmod (2 * k)%positive)
            (QSeqEquiv_cau_r xn yn cvmod cveq)).
-  exact (QCauchySeq_bounded_prop zn Pos.to_nat H0).
+  exact (QCauchySeq_bounded_prop zn id H0).
 Qed.
 
 Lemma CReal_mult_assoc : forall x y z : CReal, (x * y) * z == x * (y * z).
@@ -217,74 +210,72 @@ Proof.
   - apply (QSeqEquivEx_trans _ (fun n => proj1_sig (CReal_mult x y) n * proj1_sig z n)%Q).
     apply CReal_mult_unfold.
     destruct x as [xn limx], y as [yn limy], z as [zn limz]; unfold CReal_mult; simpl.
-    pose proof (QCauchySeq_bounded_prop xn Pos.to_nat limx) as majx.
-    pose proof (QCauchySeq_bounded_prop yn Pos.to_nat limy) as majy.
-    pose proof (QCauchySeq_bounded_prop zn Pos.to_nat limz) as majz.
-    remember (QCauchySeq_bound xn Pos.to_nat) as Ax.
-    remember (QCauchySeq_bound yn Pos.to_nat) as Ay.
-    remember (QCauchySeq_bound zn Pos.to_nat) as Az.
+    pose proof (QCauchySeq_bounded_prop xn id limx) as majx.
+    pose proof (QCauchySeq_bounded_prop yn id limy) as majy.
+    pose proof (QCauchySeq_bounded_prop zn id limz) as majz.
+    remember (QCauchySeq_bound xn id) as Ax.
+    remember (QCauchySeq_bound yn id) as Ay.
+    remember (QCauchySeq_bound zn id) as Az.
     apply CReal_mult_assoc_bounded_r. 2: exact limz.
     exists (fun p : positive =>
-         Init.Nat.max (Pos.to_nat (2 * Pos.max Ax Ay * p))
-                      (Pos.to_nat (2 * Pos.max Ax Ay * p))).
+         Pos.max (2 * Pos.max Ax Ay * p)
+                 (2 * Pos.max Ax Ay * p)).
     intros p n k H0 H1.
-    apply (CReal_mult_cauchy xn xn yn Ax Ay Pos.to_nat limx limy).
-    2: exact majy. intros. apply majx. refine (le_trans _ _ _ _ H).
-    apply le_S, le_refl. rewrite max_l in H0, H1.
-    2: apply le_refl. 2: apply le_refl.
+    apply (CReal_mult_cauchy xn xn yn Ax Ay id limx limy).
+    2: exact majy. intros. apply majx. refine (Pos.le_trans _ _ _ _ H).
+    discriminate. rewrite Pos.max_l in H0, H1.
+    2: apply Pos.le_refl. 2: apply Pos.le_refl.
     apply linear_max.
-    apply (le_trans _ (Pos.to_nat (2 * Pos.max Ax Ay * p))).
-    rewrite <- (mult_1_l (Pos.to_nat p)). rewrite Pos2Nat.inj_mul.
-    apply Nat.mul_le_mono_nonneg. auto. apply Pos2Nat.is_pos.
-    apply le_0_n. apply le_refl. apply H0. rewrite max_l. 2: apply Nat.le_max_r.
-    rewrite Nat.max_r in H1. 2: apply le_refl.
-    refine (le_trans _ _ _ _ H1). rewrite Nat.max_r.
-    apply le_refl. apply Pos2Nat.inj_le.
-    apply (Pos.le_trans _ (2*1)). apply Pos.le_refl.
+    apply (Pos.le_trans _ (2 * Pos.max Ax Ay * p)).
+    apply (Pos.le_trans _ (1*p)). apply Pos.le_refl.
+    apply Pos.mul_le_mono_r. discriminate.
+    exact H0. rewrite Pos.max_l. 2: apply Pos.le_max_r.
+    rewrite Pos.max_r in H1. 2: apply Pos.le_refl.
+    refine (Pos.le_trans _ _ _ _ H1). rewrite Pos.max_r.
+    apply Pos.le_refl. apply (Pos.le_trans _ (2*1)). apply Pos.le_refl.
+    unfold id.
     rewrite <- Pos.mul_assoc, <- (Pos.mul_le_mono_l 2 1).
     destruct (Pos.max Ax Ay * p)%positive; discriminate.
   - apply (QSeqEquivEx_trans
              _ (fun n => proj1_sig x n * proj1_sig (CReal_mult y z) n)%Q).
     2: apply QSeqEquivEx_sym; apply CReal_mult_unfold.
     destruct x as [xn limx], y as [yn limy], z as [zn limz]; unfold CReal_mult; simpl.
-    pose proof (QCauchySeq_bounded_prop xn Pos.to_nat limx) as majx.
-    pose proof (QCauchySeq_bounded_prop yn Pos.to_nat limy) as majy.
-    pose proof (QCauchySeq_bounded_prop zn Pos.to_nat limz) as majz.
-    remember (QCauchySeq_bound xn Pos.to_nat) as Ax.
-    remember (QCauchySeq_bound yn Pos.to_nat) as Ay.
-    remember (QCauchySeq_bound zn Pos.to_nat) as Az.
-    pose proof (CReal_mult_assoc_bounded_r (fun n0 : nat => yn n0 * zn n0)%Q (fun n : nat =>
-          yn (Pos.to_nat (Pos.max Ay Az)~0 * n)%nat
-          * zn (Pos.to_nat (Pos.max Ay Az)~0 * n)%nat)%Q xn)
+    pose proof (QCauchySeq_bounded_prop xn id limx) as majx.
+    pose proof (QCauchySeq_bounded_prop yn id limy) as majy.
+    pose proof (QCauchySeq_bounded_prop zn id limz) as majz.
+    remember (QCauchySeq_bound xn id) as Ax.
+    remember (QCauchySeq_bound yn id) as Ay.
+    remember (QCauchySeq_bound zn id) as Az.
+    pose proof (CReal_mult_assoc_bounded_r (fun n0 : positive => yn n0 * zn n0)%Q (fun n : positive =>
+          yn ((Pos.max Ay Az)~0 * n)%positive
+          * zn ((Pos.max Ay Az)~0 * n)%positive)%Q xn)
       as [cvmod cveq].
     + exists (fun p : positive =>
-           max (Pos.to_nat (2 * Pos.max Ay Az * p))
-               (Pos.to_nat (2 * Pos.max Ay Az * p))).
-      intros p n k H0 H1. rewrite max_l in H0, H1.
-      apply (CReal_mult_cauchy yn yn zn Ay Az Pos.to_nat limy limz).
-      2: exact majz. intros. apply majy. refine (le_trans _ _ _ _ H).
-      apply le_S, le_refl.
-      3: apply le_refl. 3: apply le_refl.
-      rewrite max_l. rewrite max_r. apply H0.
-      apply Pos2Nat.inj_le.
-      apply (Pos.le_trans _ (2*1)). apply Pos.le_refl.
+           Pos.max (2 * Pos.max Ay Az * p)
+                   (2 * Pos.max Ay Az * p)).
+      intros p n k H0 H1. rewrite Pos.max_l in H0, H1.
+      apply (CReal_mult_cauchy yn yn zn Ay Az id limy limz).
+      2: exact majz. intros. apply majy. refine (Pos.le_trans _ _ _ _ H).
+      discriminate.
+      3: apply Pos.le_refl. 3: apply Pos.le_refl.
+      rewrite Pos.max_l. rewrite Pos.max_r. apply H0.
+      apply (Pos.le_trans _ (2*1)). apply Pos.le_refl. unfold id.
       rewrite <- Pos.mul_assoc, <- (Pos.mul_le_mono_l 2 1).
       destruct (Pos.max Ay Az * p)%positive; discriminate.
-      apply Nat.le_max_r.
-      apply linear_max. refine (le_trans _ _ _ _ H1).
-      rewrite <- (mult_1_l (Pos.to_nat p)). rewrite Pos2Nat.inj_mul.
-      apply Nat.mul_le_mono_nonneg. auto. apply Pos2Nat.is_pos.
-      apply le_0_n. apply le_refl.
+      apply Pos.le_max_r.
+      apply linear_max. refine (Pos.le_trans _ _ _ _ H1).
+      apply (Pos.le_trans _ (1*p)). apply Pos.le_refl.
+      apply Pos.mul_le_mono_r. discriminate.
     + exact limx.
     + exists cvmod. intros p k n H1 H2. specialize (cveq p k n H1 H2).
       setoid_replace (xn k * yn k * zn k -
                       xn n *
-                      (yn (Pos.to_nat (Pos.max Ay Az)~0 * n)%nat *
-                       zn (Pos.to_nat (Pos.max Ay Az)~0 * n)%nat))%Q
-        with ((fun n : nat => yn n * zn n * xn n) k -
-              (fun n : nat =>
-                 yn (Pos.to_nat (Pos.max Ay Az)~0 * n)%nat *
-                 zn (Pos.to_nat (Pos.max Ay Az)~0 * n)%nat *
+                      (yn ((Pos.max Ay Az)~0 * n)%positive *
+                       zn ((Pos.max Ay Az)~0 * n)%positive))%Q
+        with ((fun n : positive => yn n * zn n * xn n) k -
+              (fun n : positive =>
+                 yn ((Pos.max Ay Az)~0 * n)%positive *
+                 zn ((Pos.max Ay Az)~0 * n)%positive *
                  xn n) n)%Q.
       apply cveq. ring.
 Qed.
@@ -295,30 +286,29 @@ Proof.
   apply (QSeqEquivEx_trans _ (fun n => proj1_sig y n * proj1_sig x n)%Q).
   destruct x as [xn limx], y as [yn limy]; simpl.
   2: apply QSeqEquivEx_sym; apply CReal_mult_unfold.
-  pose proof (QCauchySeq_bounded_prop xn Pos.to_nat limx) as majx.
-  pose proof (QCauchySeq_bounded_prop yn Pos.to_nat limy) as majy.
-  remember (QCauchySeq_bound xn Pos.to_nat) as Ax.
-  remember (QCauchySeq_bound yn Pos.to_nat) as Ay.
+  pose proof (QCauchySeq_bounded_prop xn id limx) as majx.
+  pose proof (QCauchySeq_bounded_prop yn id limy) as majy.
+  remember (QCauchySeq_bound xn id) as Ax.
+  remember (QCauchySeq_bound yn id) as Ay.
   apply QSeqEquivEx_sym.
   exists (fun p : positive =>
-       Init.Nat.max (Pos.to_nat (2 * Pos.max Ay Ax * p))
-                    (Pos.to_nat (2 * Pos.max Ay Ax * p))).
-  intros p n k H0 H1. rewrite max_l in H0, H1.
-  2: apply le_refl. 2: apply le_refl.
-  rewrite (Qmult_comm (xn (Pos.to_nat (Pos.max Ax Ay)~0 * k)%nat)).
-  apply (CReal_mult_cauchy yn yn xn Ay Ax Pos.to_nat limy limx).
-  2: exact majx. intros. apply majy. refine (le_trans _ _ _ _ H).
-  apply le_S, le_refl.
-  rewrite max_l. rewrite max_r. apply H0.
-  apply Pos2Nat.inj_le.
+       Pos.max (2 * Pos.max Ay Ax * p)
+               (2 * Pos.max Ay Ax * p)).
+  intros p n k H0 H1. rewrite Pos.max_l in H0, H1.
+  2: apply Pos.le_refl. 2: apply Pos.le_refl.
+  rewrite (Qmult_comm (xn ((Pos.max Ax Ay)~0 * k)%positive)).
+  apply (CReal_mult_cauchy yn yn xn Ay Ax id limy limx).
+  2: exact majx. intros. apply majy. refine (Pos.le_trans _ _ _ _ H).
+  discriminate.
+  rewrite Pos.max_l. rewrite Pos.max_r. apply H0.
+  unfold id.
   apply (Pos.le_trans _ (2*1)). apply Pos.le_refl.
   rewrite <- Pos.mul_assoc, <- (Pos.mul_le_mono_l 2 1).
   destruct (Pos.max Ay Ax * p)%positive; discriminate.
-  apply Nat.le_max_r. rewrite (Pos.max_comm Ax Ay).
-  apply linear_max. refine (le_trans _ _ _ _ H1).
-  rewrite <- (mult_1_l (Pos.to_nat p)). rewrite Pos2Nat.inj_mul.
-  apply Nat.mul_le_mono_nonneg. auto. apply Pos2Nat.is_pos.
-  apply le_0_n. apply le_refl.
+  apply Pos.le_max_r. rewrite (Pos.max_comm Ax Ay).
+  apply linear_max. refine (Pos.le_trans _ _ _ _ H1).
+  apply (Pos.le_trans _ (1*p)). apply Pos.le_refl.
+  apply Pos.mul_le_mono_r. discriminate.
 Qed.
 
 Lemma CReal_mult_proper_l : forall x y z : CReal,
@@ -333,16 +323,16 @@ Proof.
   apply CReal_mult_unfold.
   destruct x as [xn limx], y as [yn limy], z as [zn limz]; simpl.
   destruct H as [cvmod H]. simpl in H.
-  pose proof (QCauchySeq_bounded_prop xn Pos.to_nat limx) as majx.
+  pose proof (QCauchySeq_bounded_prop xn id limx) as majx.
   pose proof (QCauchySeq_bounded_prop
            zn (fun k => cvmod (2 * k)%positive)
            (QSeqEquiv_cau_r yn zn cvmod H)) as majz.
-  remember (QCauchySeq_bound xn Pos.to_nat) as Ax.
+  remember (QCauchySeq_bound xn id) as Ax.
   remember (QCauchySeq_bound zn (fun k => cvmod (2 * k)%positive)) as Az.
   apply QSeqEquivEx_sym.
   exists (fun p : positive =>
-       max (max (cvmod (2%positive)) (cvmod (2 * Pos.max Az Ax * p)%positive))
-           (Pos.to_nat (2 * Pos.max Az Ax * p))).
+       Pos.max (Pos.max (cvmod (2%positive)) (cvmod (2 * Pos.max Az Ax * p)%positive))
+               (2 * Pos.max Az Ax * p)).
   intros p n k H1 H2.
   setoid_replace (xn n * yn n - xn k * zn k)%Q
     with (yn n * xn n - zn k * xn k)%Q. 2: ring.
@@ -359,25 +349,21 @@ Proof.
   pose proof (CRealLt_aboveSig (inject_Q 0) x x0 H).
   pose proof (CRealLt_aboveSig (inject_Q 0) y x1 H0).
   destruct x as [xn limx], y as [yn limy]; simpl in H, H1, H2, H0.
-  pose proof (QCauchySeq_bounded_prop xn Pos.to_nat limx) as majx.
-  pose proof (QCauchySeq_bounded_prop yn Pos.to_nat limy) as majy.
-  destruct (Qarchimedean (/ (xn (Pos.to_nat x0) - 0 - (2 # x0)))).
-  destruct (Qarchimedean (/ (yn (Pos.to_nat x1) - 0 - (2 # x1)))).
+  pose proof (QCauchySeq_bounded_prop xn id limx) as majx.
+  pose proof (QCauchySeq_bounded_prop yn id limy) as majy.
+  destruct (Qarchimedean (/ (xn x0 - 0 - (2 # x0)))).
+  destruct (Qarchimedean (/ (yn x1 - 0 - (2 # x1)))).
   exists (Pos.max x0 x~0 * Pos.max x1 x2~0)%positive.
   simpl.
-  remember (QCauchySeq_bound xn Pos.to_nat) as Ax.
-  remember (QCauchySeq_bound yn Pos.to_nat) as Ay.
+  remember (QCauchySeq_bound xn id) as Ax.
+  remember (QCauchySeq_bound yn id) as Ay.
   unfold Qminus. rewrite Qplus_0_r.
-  rewrite <- Pos2Nat.inj_mul.
   unfold Qminus in H1, H2.
   specialize (H1 ((Pos.max Ax Ay)~0 * (Pos.max x0 x~0 * Pos.max x1 x2~0))%positive).
   assert (Pos.max x1 x2~0 <= (Pos.max Ax Ay)~0 * (Pos.max x0 x~0 * Pos.max x1 x2~0))%positive.
-  { apply Pos2Nat.inj_le.
-    rewrite Pos.mul_assoc. rewrite Pos2Nat.inj_mul.
-    rewrite <- (mult_1_l (Pos.to_nat (Pos.max x1 x2~0))).
-    rewrite mult_assoc. apply Nat.mul_le_mono_nonneg. auto.
-    rewrite mult_1_r. apply Pos2Nat.is_pos. apply le_0_n.
-    apply le_refl. }
+  { rewrite Pos.mul_assoc.
+    rewrite <- (Pos.mul_1_l (Pos.max x1 x2~0)).
+    rewrite Pos.mul_assoc. apply Pos.mul_le_mono_r. discriminate. }
   specialize (H2 ((Pos.max Ax Ay)~0 * (Pos.max x0 x~0 * Pos.max x1 x2~0))%positive H3).
   rewrite Qplus_0_r in H1, H2.
   apply (Qlt_trans _ ((2 # Pos.max x0 x~0) * (2 # Pos.max x1 x2~0))).
@@ -386,7 +372,7 @@ Proof.
   replace (Z.pos p~0) with (2 * Z.pos p)%Z. apply Z.mul_lt_mono_pos_r.
   apply Pos2Z.is_pos. reflexivity. reflexivity.
   apply H4.
-  apply (Qlt_trans _ ((2 # Pos.max x0 x~0) * (yn (Pos.to_nat ((Pos.max Ax Ay)~0 * (Pos.max x0 x~0 * Pos.max x1 x2~0)))))).
+  apply (Qlt_trans _ ((2 # Pos.max x0 x~0) * (yn ((Pos.max Ax Ay)~0 * (Pos.max x0 x~0 * Pos.max x1 x2~0))%positive))).
   apply Qmult_lt_l. reflexivity. apply H2. apply Qmult_lt_r.
   apply (Qlt_trans 0 (2 # Pos.max x1 x2~0)). reflexivity. apply H2.
   apply H1. rewrite Pos.mul_comm. apply Pos2Nat.inj_le.
@@ -406,140 +392,133 @@ Proof.
   apply CReal_mult_unfold.
   apply (QSeqEquivEx_trans _ (fun n => proj1_sig (CReal_mult x y) n
                                     + proj1_sig (CReal_mult x z) n))%Q.
-  2: apply QSeqEquivEx_sym; exists (fun p => Pos.to_nat (2 * p))
+  2: apply QSeqEquivEx_sym; exists (fun p:positive => 2 * p)%positive
   ; apply CReal_plus_unfold.
   apply (QSeqEquivEx_trans _ (fun n => proj1_sig x n
                                     * (proj1_sig y n + proj1_sig z n))%Q).
   - pose proof (CReal_plus_unfold y z).
     destruct x as [xn limx], y as [yn limy], z as [zn limz]; simpl; simpl in H.
-    pose proof (QCauchySeq_bounded_prop xn Pos.to_nat) as majx.
-    pose proof (QCauchySeq_bounded_prop yn Pos.to_nat) as majy.
-    pose proof (QCauchySeq_bounded_prop zn Pos.to_nat) as majz.
-    remember (QCauchySeq_bound xn Pos.to_nat) as Ax.
-    remember (QCauchySeq_bound yn Pos.to_nat) as Ay.
-    remember (QCauchySeq_bound zn Pos.to_nat) as Az.
-    pose proof (CReal_mult_cauchy (fun n => yn (n + (n + 0))%nat + zn (n + (n + 0))%nat)%Q
+    pose proof (QCauchySeq_bounded_prop xn id) as majx.
+    pose proof (QCauchySeq_bounded_prop yn id) as majy.
+    pose proof (QCauchySeq_bounded_prop zn id) as majz.
+    remember (QCauchySeq_bound xn id) as Ax.
+    remember (QCauchySeq_bound yn id) as Ay.
+    remember (QCauchySeq_bound zn id) as Az.
+    pose proof (CReal_mult_cauchy (fun n => yn (n~0)%positive + zn (n~0)%positive)%Q
                                   (fun n => yn n + zn n)%Q
                                   xn (Ay + Az) Ax
-                                  (fun p => Pos.to_nat (2 * p)) H limx).
-    exists (fun p : positive => (Pos.to_nat (2 * (2 * Pos.max (Ay + Az) Ax * p)))).
+                                  (fun p:positive => 2 * p)%positive H limx).
+    exists (fun p : positive => (2 * (2 * Pos.max (Ay + Az) Ax * p))%positive).
     intros p n k H1 H2.
-    setoid_replace (xn n * (yn (n + (n + 0))%nat + zn (n + (n + 0))%nat) - xn k * (yn k + zn k))%Q
-      with ((yn (n + (n + 0))%nat + zn (n + (n + 0))%nat) * xn n - (yn k + zn k) * xn k)%Q.
+    setoid_replace (xn n * (yn (n~0)%positive + zn (n~0)%positive) - xn k * (yn k + zn k))%Q
+      with ((yn (n~0)%positive + zn (n~0)%positive) * xn n - (yn k + zn k) * xn k)%Q.
     2: ring.
-    assert (Pos.to_nat (2 * Pos.max (Ay + Az) Ax * p) <=
-            Pos.to_nat 2 * Pos.to_nat (2 * Pos.max (Ay + Az) Ax * p))%nat.
-    { rewrite (Pos2Nat.inj_mul 2).
-      rewrite <- (mult_1_l (Pos.to_nat (2 * Pos.max (Ay + Az) Ax * p))).
-      rewrite mult_assoc. apply Nat.mul_le_mono_nonneg. auto.
-      simpl. auto. apply le_0_n. apply le_refl. }
+    assert ((2 * Pos.max (Ay + Az) Ax * p) <=
+            2 * (2 * Pos.max (Ay + Az) Ax * p))%positive.
+    { rewrite <- Pos.mul_assoc.
+      apply Pos.mul_le_mono_l.
+      apply (Pos.le_trans _ (1*(Pos.max (Ay + Az) Ax * p))).
+      apply Pos.le_refl. apply Pos.mul_le_mono_r. discriminate. }
     apply H0. intros n0 H4.
     apply (Qle_lt_trans _ _ _ (Qabs_triangle _ _)).
     rewrite Pos2Z.inj_add, <- Qinv_plus_distr. apply Qplus_lt_le_compat.
     apply majy. exact limy.
-    refine (le_trans _ _ _ _ H4); apply le_n_S, le_0_n.
+    refine (Pos.le_trans _ _ _ _ H4); discriminate.
     apply Qlt_le_weak. apply majz. exact limz.
-    refine (le_trans _ _ _ _ H4); apply le_n_S, le_0_n.
-    apply majx. exact limx. refine (le_trans _ _ _ _ H1).
-    rewrite max_l. rewrite max_r. apply le_refl.
-    apply Pos2Nat.inj_le. rewrite <- (Pos.mul_le_mono_l 2).
+    refine (Pos.le_trans _ _ _ _ H4); discriminate.
+    apply majx. exact limx. refine (Pos.le_trans _ _ _ _ H1).
+    rewrite Pos.max_l. rewrite Pos.max_r. apply Pos.le_refl.
+    rewrite <- (Pos.mul_le_mono_l 2).
     apply (Pos.le_trans _ (2*1)). apply Pos.le_refl.
     rewrite <- Pos.mul_assoc, <- Pos.mul_le_mono_l.
     destruct (Pos.max (Ay + Az) Ax * p)%positive; discriminate.
-    apply (le_trans _ (Pos.to_nat (2 * (2 * Pos.max (Ay + Az) Ax * p)))).
-    2: apply Nat.le_max_r. apply Pos2Nat.inj_le.
+    apply (Pos.le_trans _ (2 * (2 * Pos.max (Ay + Az) Ax * p))).
+    2: apply Pos.le_max_r.
     rewrite <- Pos.mul_assoc. rewrite (Pos.mul_assoc 2 2).
     rewrite <- Pos.mul_le_mono_r. discriminate.
-    refine (le_trans _ _ _ _ H2). rewrite <- Nat.max_comm.
-    rewrite Nat.max_assoc. rewrite max_r. apply le_refl.
-    apply Nat.max_lub.
-    rewrite <- Pos2Nat.inj_mul in H3. apply H3. apply Pos2Nat.inj_le.
+    refine (Pos.le_trans _ _ _ _ H2). rewrite <- Pos.max_comm.
+    rewrite Pos.max_assoc. rewrite Pos.max_r. apply Pos.le_refl.
+    apply Pos.max_lub. apply H3.
     rewrite <- Pos.mul_le_mono_l.
     apply (Pos.le_trans _ (2*1)). apply Pos.le_refl.
     rewrite <- Pos.mul_assoc, <- Pos.mul_le_mono_l.
     destruct (Pos.max (Ay + Az) Ax * p)%positive; discriminate.
   - destruct x as [xn limx], y as [yn limy], z as [zn limz]; simpl.
-    pose proof (QCauchySeq_bounded_prop xn Pos.to_nat) as majx.
-    pose proof (QCauchySeq_bounded_prop yn Pos.to_nat) as majy.
-    pose proof (QCauchySeq_bounded_prop zn Pos.to_nat) as majz.
-    remember (QCauchySeq_bound xn Pos.to_nat) as Ax.
-    remember (QCauchySeq_bound yn Pos.to_nat) as Ay.
-    remember (QCauchySeq_bound zn Pos.to_nat) as Az.
-    exists (fun p : positive => (Pos.to_nat (2 * (Pos.max (Pos.max Ax Ay) Az) * (2 * p)))).
+    pose proof (QCauchySeq_bounded_prop xn id) as majx.
+    pose proof (QCauchySeq_bounded_prop yn id) as majy.
+    pose proof (QCauchySeq_bounded_prop zn id) as majz.
+    remember (QCauchySeq_bound xn id) as Ax.
+    remember (QCauchySeq_bound yn id) as Ay.
+    remember (QCauchySeq_bound zn id) as Az.
+    exists (fun p : positive => (2 * (Pos.max (Pos.max Ax Ay) Az) * (2 * p))%positive).
     intros p n k H H0.
     setoid_replace (xn n * (yn n + zn n) -
-     (xn (Pos.to_nat (Pos.max Ax Ay)~0 * k)%nat *
-      yn (Pos.to_nat (Pos.max Ax Ay)~0 * k)%nat +
-      xn (Pos.to_nat (Pos.max Ax Az)~0 * k)%nat *
-      zn (Pos.to_nat (Pos.max Ax Az)~0 * k)%nat))%Q
-      with (xn n * yn n - (xn (Pos.to_nat (Pos.max Ax Ay)~0 * k)%nat *
-                           yn (Pos.to_nat (Pos.max Ax Ay)~0 * k)%nat)
-            + (xn n * zn n - xn (Pos.to_nat (Pos.max Ax Az)~0 * k)%nat *
-                             zn (Pos.to_nat (Pos.max Ax Az)~0 * k)%nat))%Q.
+     (xn ((Pos.max Ax Ay)~0 * k)%positive *
+      yn ((Pos.max Ax Ay)~0 * k)%positive +
+      xn ((Pos.max Ax Az)~0 * k)%positive *
+      zn ((Pos.max Ax Az)~0 * k)%positive))%Q
+      with (xn n * yn n - (xn ((Pos.max Ax Ay)~0 * k)%positive *
+                           yn ((Pos.max Ax Ay)~0 * k)%positive)
+            + (xn n * zn n - xn ((Pos.max Ax Az)~0 * k)%positive *
+                             zn ((Pos.max Ax Az)~0 * k)%positive))%Q.
     2: ring.
-    apply (Qle_lt_trans _ (Qabs (xn n * yn n - (xn (Pos.to_nat (Pos.max Ax Ay)~0 * k)%nat *
-                                                yn (Pos.to_nat (Pos.max Ax Ay)~0 * k)%nat))
-                           + Qabs (xn n * zn n - xn (Pos.to_nat (Pos.max Ax Az)~0 * k)%nat *
-                             zn (Pos.to_nat (Pos.max Ax Az)~0 * k)%nat))).
+    apply (Qle_lt_trans _ (Qabs (xn n * yn n - (xn ((Pos.max Ax Ay)~0 * k)%positive *
+                                                yn ((Pos.max Ax Ay)~0 * k)%positive))
+                           + Qabs (xn n * zn n - xn ((Pos.max Ax Az)~0 * k)%positive *
+                             zn ((Pos.max Ax Az)~0 * k)%positive))).
     apply Qabs_triangle.
     setoid_replace (1#p)%Q with ((1#2*p) + (1#2*p))%Q.
     apply Qplus_lt_le_compat.
-    + apply (CReal_mult_cauchy xn xn yn Ax Ay Pos.to_nat limx limy).
+    + apply (CReal_mult_cauchy xn xn yn Ax Ay id limx limy).
       intros. apply majx. exact limx.
-      refine (le_trans _ _ _ _ H1). apply le_S, le_refl.
+      refine (Pos.le_trans _ _ _ _ H1). discriminate.
       apply majy. exact limy.
-      rewrite <- Nat.max_assoc.
-      rewrite (Nat.max_l ((Pos.to_nat (2 * Pos.max Ax Ay * (2 * p))))).
-      2: apply le_refl.
-      refine (le_trans _ _ _ _ H). apply Nat.max_lub.
-      apply Pos2Nat.inj_le. apply (Pos.le_trans _ (2*1)).
+      rewrite <- Pos.max_assoc.
+      rewrite (Pos.max_l ((2 * Pos.max Ax Ay * (2 * p)))).
+      2: apply Pos.le_refl.
+      refine (Pos.le_trans _ _ _ _ H). apply Pos.max_lub.
+      apply (Pos.le_trans _ (2*1)).
       apply Pos.le_refl. rewrite <- Pos.mul_assoc, <- Pos.mul_le_mono_l.
       destruct (Pos.max (Pos.max Ax Ay) Az * (2 * p))%positive; discriminate.
-      apply Pos2Nat.inj_le.
       rewrite <- Pos.mul_assoc, <- Pos.mul_assoc.
       rewrite <- Pos.mul_le_mono_l, <- Pos.mul_le_mono_r.
       apply Pos.le_max_l.
-      rewrite <- Nat.max_assoc.
-      rewrite (Nat.max_l ((Pos.to_nat (2 * Pos.max Ax Ay * (2 * p))))).
-      2: apply le_refl.
-      rewrite max_r. apply (le_trans _ (1*k)).
-      rewrite Nat.mul_1_l. refine (le_trans _ _ _ _ H0).
-      apply Pos2Nat.inj_le.
+      rewrite <- Pos.max_assoc.
+      rewrite (Pos.max_l ((2 * Pos.max Ax Ay * (2 * p)))).
+      2: apply Pos.le_refl.
+      rewrite Pos.max_r. apply (Pos.le_trans _ (1*k)).
+      rewrite Pos.mul_1_l. refine (Pos.le_trans _ _ _ _ H0).
       rewrite <- Pos.mul_assoc, <- Pos.mul_assoc, <- Pos.mul_le_mono_l.
       rewrite <- Pos.mul_le_mono_r.
-      apply Pos.le_max_l. apply Nat.mul_le_mono_nonneg_r. apply le_0_n.
-      apply Pos2Nat.is_pos. apply Pos2Nat.inj_le.
+      apply Pos.le_max_l. apply Pos.mul_le_mono_r. discriminate.
       apply (Pos.le_trans _ (2*1)). apply Pos.le_refl.
       rewrite <- Pos.mul_assoc, <- Pos.mul_le_mono_l.
       destruct (Pos.max Ax Ay * (2 * p))%positive; discriminate.
     + apply Qlt_le_weak.
-      apply (CReal_mult_cauchy xn xn zn Ax Az Pos.to_nat limx limz).
+      apply (CReal_mult_cauchy xn xn zn Ax Az id limx limz).
       intros. apply majx. exact limx.
-      refine (le_trans _ _ _ _ H1). apply le_S, le_refl.
+      refine (Pos.le_trans _ _ _ _ H1). discriminate.
       intros. apply majz. exact limz. exact H1.
-      rewrite <- Nat.max_assoc.
-      rewrite (Nat.max_l ((Pos.to_nat (2 * Pos.max Ax Az * (2 * p))))).
-      2: apply le_refl.
-      refine (le_trans _ _ _ _ H). apply Nat.max_lub.
-      apply Pos2Nat.inj_le. apply (Pos.le_trans _ (2*1)).
+      rewrite <- Pos.max_assoc.
+      rewrite (Pos.max_l ((2 * Pos.max Ax Az * (2 * p)))).
+      2: apply Pos.le_refl.
+      refine (Pos.le_trans _ _ _ _ H). apply Pos.max_lub.
+      apply (Pos.le_trans _ (2*1)).
       apply Pos.le_refl. rewrite <- Pos.mul_assoc, <- Pos.mul_le_mono_l.
       destruct (Pos.max (Pos.max Ax Ay) Az * (2 * p))%positive; discriminate.
-      apply Pos2Nat.inj_le.
       rewrite <- Pos.mul_assoc, <- Pos.mul_assoc.
       rewrite <- Pos.mul_le_mono_l, <- Pos.mul_le_mono_r.
       rewrite <- Pos.max_assoc, (Pos.max_comm Ay Az), Pos.max_assoc.
       apply Pos.le_max_l.
-      rewrite <- Nat.max_assoc.
-      rewrite (Nat.max_l ((Pos.to_nat (2 * Pos.max Ax Az * (2 * p))))).
-      2: apply le_refl.
-      rewrite max_r. apply (le_trans _ (1*k)).
-      rewrite Nat.mul_1_l. refine (le_trans _ _ _ _ H0).
-      apply Pos2Nat.inj_le.
+      rewrite <- Pos.max_assoc.
+      rewrite (Pos.max_l ((2 * Pos.max Ax Az * (2 * p)))).
+      2: apply Pos.le_refl.
+      rewrite Pos.max_r. apply (Pos.le_trans _ (1*k)).
+      rewrite Pos.mul_1_l. refine (Pos.le_trans _ _ _ _ H0).
       rewrite <- Pos.mul_assoc, <- Pos.mul_assoc, <- Pos.mul_le_mono_l.
       rewrite <- Pos.mul_le_mono_r.
       rewrite <- Pos.max_assoc, (Pos.max_comm Ay Az), Pos.max_assoc.
-      apply Pos.le_max_l. apply Nat.mul_le_mono_nonneg_r. apply le_0_n.
-      apply Pos2Nat.is_pos. apply Pos2Nat.inj_le.
+      apply Pos.le_max_l. apply Pos.mul_le_mono_r. discriminate.
       apply (Pos.le_trans _ (2*1)). apply Pos.le_refl.
       rewrite <- Pos.mul_assoc, <- Pos.mul_le_mono_l.
       destruct (Pos.max Ax Az * (2 * p))%positive; discriminate.
@@ -560,38 +539,37 @@ Proof.
   intros [rn limr]. split.
   - intros [m maj]. simpl in maj.
     rewrite Qmult_1_l in maj.
-    pose proof (QCauchySeq_bounded_prop (fun _ : nat => 1%Q) Pos.to_nat (ConstCauchy 1)).
-    pose proof (QCauchySeq_bounded_prop rn Pos.to_nat limr).
-    remember (QCauchySeq_bound (fun _ : nat => 1%Q) Pos.to_nat) as x.
-    remember (QCauchySeq_bound rn Pos.to_nat) as x0.
+    pose proof (QCauchySeq_bounded_prop (fun _ : positive => 1%Q) id (ConstCauchy 1)).
+    pose proof (QCauchySeq_bounded_prop rn id limr).
+    remember (QCauchySeq_bound (fun _ : positive => 1%Q) id) as x.
+    remember (QCauchySeq_bound rn id) as x0.
     specialize (limr m).
     apply (Qlt_not_le (2 # m) (1 # m)).
-    apply (Qlt_trans _ (rn (Pos.to_nat m)
-                        - rn (Pos.to_nat (Pos.max x x0)~0 * Pos.to_nat m)%nat)).
+    apply (Qlt_trans _ (rn m
+                        - rn ((Pos.max x x0)~0 * m)%positive)).
     apply maj.
-    apply (Qle_lt_trans _ (Qabs (rn (Pos.to_nat m) - rn (Pos.to_nat (Pos.max x x0)~0 * Pos.to_nat m)%nat))).
-    apply Qle_Qabs. apply limr. apply le_refl.
-    rewrite <- (mult_1_l (Pos.to_nat m)). rewrite mult_assoc.
-    apply Nat.mul_le_mono_nonneg. auto. rewrite mult_1_r.
-    apply Pos2Nat.is_pos. apply le_0_n. apply le_refl.
+    apply (Qle_lt_trans _ (Qabs (rn m - rn ((Pos.max x x0)~0 * m)%positive))).
+    apply Qle_Qabs. apply limr. apply Pos.le_refl.
+    rewrite <- (Pos.mul_1_l m). rewrite Pos.mul_assoc. unfold id.
+    apply Pos.mul_le_mono_r. discriminate.
     apply Z.mul_le_mono_nonneg. discriminate. discriminate.
     discriminate. apply Z.le_refl.
   - intros [m maj]. simpl in maj.
-    pose proof (QCauchySeq_bounded_prop (fun _ : nat => 1%Q) Pos.to_nat (ConstCauchy 1)).
-    pose proof (QCauchySeq_bounded_prop rn Pos.to_nat limr).
-    remember (QCauchySeq_bound (fun _ : nat => 1%Q) Pos.to_nat) as x.
-    remember (QCauchySeq_bound rn Pos.to_nat) as x0.
+    pose proof (QCauchySeq_bounded_prop (fun _ : positive => 1%Q) id (ConstCauchy 1)).
+    pose proof (QCauchySeq_bounded_prop rn id limr).
+    remember (QCauchySeq_bound (fun _ : positive => 1%Q) id) as x.
+    remember (QCauchySeq_bound rn id) as x0.
     simpl in maj. rewrite Qmult_1_l in maj.
     specialize (limr m).
     apply (Qlt_not_le (2 # m) (1 # m)).
-    apply (Qlt_trans _ (rn (Pos.to_nat (Pos.max x x0)~0 * Pos.to_nat m)%nat - rn (Pos.to_nat m))).
+    apply (Qlt_trans _ (rn ((Pos.max x x0)~0 * m)%positive - rn m)).
     apply maj.
-    apply (Qle_lt_trans _ (Qabs (rn (Pos.to_nat (Pos.max x x0)~0 * Pos.to_nat m)%nat - rn (Pos.to_nat m)))).
+    apply (Qle_lt_trans _ (Qabs (rn ((Pos.max x x0)~0 * m)%positive - rn m))).
     apply Qle_Qabs. apply limr.
-    rewrite <- (mult_1_l (Pos.to_nat m)). rewrite mult_assoc.
-    apply Nat.mul_le_mono_nonneg. auto. rewrite mult_1_r.
-    apply Pos2Nat.is_pos. apply le_0_n. apply le_refl.
-    apply le_refl. apply Z.mul_le_mono_nonneg. discriminate. discriminate.
+    rewrite <- (Pos.mul_1_l m). rewrite Pos.mul_assoc. unfold id.
+    apply Pos.mul_le_mono_r. discriminate.
+    apply Pos.le_refl.
+    apply Z.mul_le_mono_nonneg. discriminate. discriminate.
     discriminate. apply Z.le_refl.
 Qed.
 
@@ -748,11 +726,11 @@ Proof.
 Qed.
 
 Lemma CReal_abs_appart_zero : forall (x : CReal) (n : positive),
-    Qlt (2#n) (Qabs (proj1_sig x (Pos.to_nat n)))
+    Qlt (2#n) (Qabs (proj1_sig x n))
     -> 0 # x.
 Proof.
   intros. destruct x as [xn xcau]. simpl in H.
-  destruct (Qlt_le_dec 0 (xn (Pos.to_nat n))).
+  destruct (Qlt_le_dec 0 (xn n)).
   - left. exists n; simpl. rewrite Qabs_pos in H.
     ring_simplify. exact H. apply Qlt_le_weak. exact q.
   - right. exists n; simpl. rewrite Qabs_neg in H.
@@ -769,39 +747,40 @@ Lemma CRealArchimedean
 Proof.
   (* Locate x within 1/4 and pick the first integer above this interval. *)
   intros [xn limx].
-  pose proof (Qlt_floor (xn 4%nat + (1#4))). unfold inject_Z in H.
-  pose proof (Qfloor_le (xn 4%nat + (1#4))). unfold inject_Z in H0.
-  remember (Qfloor (xn 4%nat + (1#4)))%Z as n.
+  pose proof (Qlt_floor (xn 4%positive + (1#4))). unfold inject_Z in H.
+  pose proof (Qfloor_le (xn 4%positive + (1#4))). unfold inject_Z in H0.
+  remember (Qfloor (xn 4%positive + (1#4)))%Z as n.
   exists (n+1)%Z. split.
-  - assert (Qlt 0 ((n + 1 # 1) - (xn 4%nat + (1 # 4)))) as epsPos.
+  - assert (Qlt 0 ((n + 1 # 1) - (xn 4%positive + (1 # 4)))) as epsPos.
     { unfold Qminus. rewrite <- Qlt_minus_iff. exact H. }
-    destruct (Qarchimedean (/((1#2)*((n + 1 # 1) - (xn 4%nat + (1 # 4)))))) as [k kmaj].
+    destruct (Qarchimedean (/((1#2)*((n + 1 # 1) - (xn 4%positive + (1 # 4)))))) as [k kmaj].
     exists (Pos.max 4 k). simpl.
-    apply (Qlt_trans _ ((n + 1 # 1) - (xn 4%nat + (1 # 4)))).
+    apply (Qlt_trans _ ((n + 1 # 1) - (xn 4%positive + (1 # 4)))).
     + setoid_replace (Z.pos k # 1)%Q with (/(1#k))%Q in kmaj. 2: reflexivity.
       rewrite <- Qinv_lt_contravar in kmaj. 2: reflexivity.
       apply (Qle_lt_trans _ (2#k)).
       rewrite <- (Qmult_le_l _ _ (1#2)).
       setoid_replace ((1 # 2) * (2 # k))%Q with (1#k)%Q. 2: reflexivity.
-      setoid_replace ((1 # 2) * (2 # Pos.max 4 k))%Q with (1#Pos.max 4 k)%Q. 2: reflexivity.
+      setoid_replace ((1 # 2) * (2 # Pos.max 4 k))%Q with (1#Pos.max 4 k)%Q.
+      2: reflexivity.
       unfold Qle; simpl. apply Pos2Z.pos_le_pos. apply Pos.le_max_r.
       reflexivity.
       rewrite <- (Qmult_lt_l _ _ (1#2)).
       setoid_replace ((1 # 2) * (2 # k))%Q with (1#k)%Q. exact kmaj.
       reflexivity. reflexivity. rewrite <- (Qmult_0_r (1#2)).
       rewrite Qmult_lt_l. exact epsPos. reflexivity.
-    + rewrite <- (Qplus_lt_r _ _ (xn (Pos.to_nat (Pos.max 4 k)) - (n + 1 # 1) + (1#4))).
+    + rewrite <- (Qplus_lt_r _ _ (xn (Pos.max 4 k) - (n + 1 # 1) + (1#4))).
       ring_simplify.
-      apply (Qle_lt_trans _ (Qabs (xn (Pos.to_nat (Pos.max 4 k)) - xn 4%nat))).
+      apply (Qle_lt_trans _ (Qabs (xn (Pos.max 4 k) - xn 4%positive))).
       apply Qle_Qabs. apply limx.
-      rewrite Pos2Nat.inj_max. apply Nat.le_max_l. apply le_refl.
+      apply Pos.le_max_l. apply Pos.le_refl.
   - apply (CReal_plus_lt_reg_l (-(2))). ring_simplify.
     exists 4%positive. simpl.
     rewrite <- Qinv_plus_distr.
     rewrite <- (Qplus_lt_r _ _ ((n#1) - (1#2))). ring_simplify.
-    apply (Qle_lt_trans _ (xn 4%nat + (1 # 4)) _ H0).
+    apply (Qle_lt_trans _ (xn 4%positive + (1 # 4)) _ H0).
     unfold Pos.to_nat; simpl.
-    rewrite <- (Qplus_lt_r _ _ (-xn 4%nat)). ring_simplify.
+    rewrite <- (Qplus_lt_r _ _ (-xn 4%positive)). ring_simplify.
     reflexivity.
 Defined.
 
@@ -821,9 +800,10 @@ Lemma CRealLtDisjunctEpsilon : forall a b c d : CReal,
     (CRealLtProp a b \/ CRealLtProp c d) -> CRealLt a b  +  CRealLt c d.
 Proof.
   intros.
+  (* Convert to nat to use indefinite description. *)
   assert (exists n : nat, n <> O /\
-             (Qlt (2 # Pos.of_nat n) (proj1_sig b n - proj1_sig a n)
-              \/ Qlt (2 # Pos.of_nat n) (proj1_sig d n - proj1_sig c n))).
+             (Qlt (2 # Pos.of_nat n) (proj1_sig b (Pos.of_nat n) - proj1_sig a (Pos.of_nat n))
+              \/ Qlt (2 # Pos.of_nat n) (proj1_sig d (Pos.of_nat n) - proj1_sig c (Pos.of_nat n)))).
   { destruct H. destruct H as [n maj]. exists (Pos.to_nat n). split.
     intro abs. destruct (Pos2Nat.is_succ n). rewrite H in abs.
     inversion abs. left. rewrite Pos2Nat.id. apply maj.
@@ -833,72 +813,73 @@ Proof.
   apply constructive_indefinite_ground_description_nat in H0.
   - destruct H0 as [n [nPos maj]].
     destruct (Qlt_le_dec (2 # Pos.of_nat n)
-                         (proj1_sig b n - proj1_sig a n)).
-    left. exists (Pos.of_nat n). rewrite Nat2Pos.id. apply q. apply nPos.
-    assert (2 # Pos.of_nat n < proj1_sig d n - proj1_sig c n)%Q.
+                         (proj1_sig b (Pos.of_nat n) - proj1_sig a (Pos.of_nat n))).
+    left. exists (Pos.of_nat n). apply q.
+    assert (2 # Pos.of_nat n < proj1_sig d (Pos.of_nat n) - proj1_sig c (Pos.of_nat n))%Q.
     destruct maj. exfalso.
-    apply (Qlt_not_le (2 # Pos.of_nat n) (proj1_sig b n - proj1_sig a n)); assumption.
-    assumption. clear maj. right. exists (Pos.of_nat n). rewrite Nat2Pos.id.
-    apply H0. apply nPos.
+    apply (Qlt_not_le (2 # Pos.of_nat n) (proj1_sig b (Pos.of_nat n) - proj1_sig a (Pos.of_nat n))); assumption.
+    assumption. clear maj. right. exists (Pos.of_nat n).
+    apply H0.
   - clear H0. clear H. intro n. destruct n. right.
     intros [abs _]. exact (abs (eq_refl O)).
-    destruct (Qlt_le_dec (2 # Pos.of_nat (S n)) (proj1_sig b (S n) - proj1_sig a (S n))).
+    destruct (Qlt_le_dec (2 # Pos.of_nat (S n)) (proj1_sig b (Pos.of_nat (S n)) - proj1_sig a (Pos.of_nat (S n)))).
     left. split. discriminate. left. apply q.
-    destruct (Qlt_le_dec (2 # Pos.of_nat (S n)) (proj1_sig d (S n) - proj1_sig c (S n))).
+    destruct (Qlt_le_dec (2 # Pos.of_nat (S n)) (proj1_sig d (Pos.of_nat (S n)) - proj1_sig c (Pos.of_nat (S n)))).
     left. split. discriminate. right. apply q0.
     right. intros [_ [abs|abs]].
     apply (Qlt_not_le (2 # Pos.of_nat (S n))
-                      (proj1_sig b (S n) - proj1_sig a (S n))); assumption.
+                      (proj1_sig b (Pos.of_nat (S n)) - proj1_sig a (Pos.of_nat (S n)))); assumption.
     apply (Qlt_not_le (2 # Pos.of_nat (S n))
-                      (proj1_sig d (S n) - proj1_sig c (S n))); assumption.
+                      (proj1_sig d (Pos.of_nat (S n)) - proj1_sig c (Pos.of_nat (S n)))); assumption.
 Qed.
 
-Lemma CRealShiftReal : forall (x : CReal) (k : nat),
-    QCauchySeq (fun n => proj1_sig x (plus n k)) Pos.to_nat.
+Lemma CRealShiftReal : forall (x : CReal) (k : positive),
+    QCauchySeq (fun n => proj1_sig x (Pos.add n k)) id.
 Proof.
-  intros x k n p q H H0.
+  assert (forall p k : positive, (p <= p + k)%positive).
+  { intros. apply Pos2Nat.inj_le. rewrite Pos2Nat.inj_add.
+    apply (le_trans _ (Pos.to_nat p + 0)).
+    rewrite plus_0_r. apply le_refl. apply Nat.add_le_mono_l.
+    apply le_0_n. }
+  intros x k n p q H0 H1.
   destruct x as [xn cau]; unfold proj1_sig.
-  destruct k. rewrite plus_0_r. rewrite plus_0_r. apply cau; assumption.
-  specialize (cau (n + Pos.of_nat (S k))%positive (p + S k)%nat (q + S k)%nat).
-  apply (Qlt_trans _ (1 # n + Pos.of_nat (S k))).
-  apply cau. rewrite Pos2Nat.inj_add. rewrite Nat2Pos.id.
-  apply Nat.add_le_mono_r. apply H. discriminate.
-  rewrite Pos2Nat.inj_add. rewrite Nat2Pos.id.
-  apply Nat.add_le_mono_r. apply H0. discriminate.
-  apply Pos2Nat.inj_lt; simpl. rewrite Pos2Nat.inj_add.
-  rewrite <- (plus_0_r (Pos.to_nat n)). rewrite <- plus_assoc.
-  apply Nat.add_lt_mono_l. apply Pos2Nat.is_pos.
+  apply cau. apply (Pos.le_trans _ _ _ H0). apply H.
+  apply (Pos.le_trans _ _ _ H1). apply H.
 Qed.
 
-Lemma CRealShiftEqual : forall (x : CReal) (k : nat),
-    CRealEq x (exist _ (fun n => proj1_sig x (plus n k)) (CRealShiftReal x k)).
+Lemma CRealShiftEqual : forall (x : CReal) (k : positive),
+    CRealEq x (exist _ (fun n => proj1_sig x (Pos.add n k)) (CRealShiftReal x k)).
 Proof.
   intros. split.
   - intros [n maj]. destruct x as [xn cau]; simpl in maj.
-    specialize (cau n (Pos.to_nat n + k)%nat (Pos.to_nat n)).
+    specialize (cau n (n + k)%positive n).
     apply Qlt_not_le in maj. apply maj. clear maj.
-    apply (Qle_trans _ (Qabs (xn (Pos.to_nat n + k)%nat - xn (Pos.to_nat n)))).
+    apply (Qle_trans _ (Qabs (xn (n + k)%positive - xn n))).
     apply Qle_Qabs. apply (Qle_trans _ (1#n)). apply Zlt_le_weak.
-    apply cau. rewrite <- (plus_0_r (Pos.to_nat n)).
-    rewrite <- plus_assoc. apply Nat.add_le_mono_l. apply le_0_n.
-    apply le_refl. apply Z.mul_le_mono_pos_r. apply Pos2Z.is_pos.
-    discriminate.
+    apply cau. unfold id. apply Pos2Nat.inj_le. rewrite Pos2Nat.inj_add.
+    apply (le_trans _ (Pos.to_nat n + 0)).
+    rewrite plus_0_r. apply le_refl. apply Nat.add_le_mono_l.
+    apply le_0_n. apply Pos.le_refl.
+    apply Z.mul_le_mono_pos_r. apply Pos2Z.is_pos. discriminate.
   - intros [n maj]. destruct x as [xn cau]; simpl in maj.
-    specialize (cau n (Pos.to_nat n) (Pos.to_nat n + k)%nat).
+    specialize (cau n n (n + k)%positive).
     apply Qlt_not_le in maj. apply maj. clear maj.
-    apply (Qle_trans _ (Qabs (xn (Pos.to_nat n) - xn (Pos.to_nat n + k)%nat))).
+    apply (Qle_trans _ (Qabs (xn n - xn (n + k)%positive))).
     apply Qle_Qabs. apply (Qle_trans _ (1#n)). apply Zlt_le_weak.
-    apply cau. apply le_refl. rewrite <- (plus_0_r (Pos.to_nat n)).
-    rewrite <- plus_assoc. apply Nat.add_le_mono_l. apply le_0_n.
+    apply cau. apply Pos.le_refl.
+    apply Pos2Nat.inj_le. rewrite Pos2Nat.inj_add.
+    apply (le_trans _ (Pos.to_nat n + 0)).
+    rewrite plus_0_r. apply le_refl. apply Nat.add_le_mono_l.
+    apply le_0_n.
     apply Z.mul_le_mono_pos_r. apply Pos2Z.is_pos. discriminate.
 Qed.
 
 (* Find an equal negative real number, which rational sequence
    stays below 0, so that it can be inversed. *)
 Definition CRealNegShift (x : CReal)
-  : CRealLt x (inject_Q 0)
-    -> { y : prod positive CReal | CRealEq x (snd y)
-                                   /\ forall n:nat, Qlt (proj1_sig (snd y) n) (-1 # fst y) }.
+  : x < inject_Q 0
+    -> { y : prod positive CReal
+      | x == (snd y) /\ forall n:positive, Qlt (proj1_sig (snd y) n) (-1 # fst y) }.
 Proof.
   intro xNeg.
   pose proof (CRealLt_aboveSig x (inject_Q 0)).
@@ -906,36 +887,26 @@ Proof.
   pose proof (CRealShiftEqual x).
   destruct xNeg as [n maj], x as [xn cau]; simpl in maj.
   specialize (H n maj); simpl in H.
-  destruct (Qarchimedean (/ (0 - xn (Pos.to_nat n) - (2 # n)))) as [a _].
+  destruct (Qarchimedean (/ (0 - xn n - (2 # n)))) as [a _].
   remember (Pos.max n a~0) as k.
   clear Heqk. clear maj. clear n.
-  exists (pair k
-          (exist _ (fun n => xn (plus n (Pos.to_nat k))) (H0 (Pos.to_nat k)))).
+  exists (pair k (exist _ (fun n => xn (Pos.add n k)) (H0 k))).
   split. apply H1. intro n. simpl. apply Qlt_minus_iff.
-  destruct n.
-  - specialize (H k).
-    unfold Qminus in H. rewrite Qplus_0_l in H. apply Qlt_minus_iff in H.
-    unfold Qminus. rewrite Qplus_comm.
-    apply (Qlt_trans _ (- xn (Pos.to_nat k)%nat - (2 #k))). apply H.
-    unfold Qminus. simpl. apply Qplus_lt_r.
-    apply Z.mul_lt_mono_pos_r. simpl. apply Pos2Z.is_pos.
-    reflexivity. apply Pos.le_refl.
-  - apply (Qlt_trans _ (-(2 # k) - xn (S n + Pos.to_nat k)%nat)).
-    rewrite <- (Nat2Pos.id (S n)). rewrite <- Pos2Nat.inj_add.
-    specialize (H (Pos.of_nat (S n) + k)%positive).
-    unfold Qminus in H. rewrite Qplus_0_l in H. apply Qlt_minus_iff in H.
-    unfold Qminus. rewrite Qplus_comm. apply H. apply Pos2Nat.inj_le.
-    rewrite <- (plus_0_l (Pos.to_nat k)). rewrite Pos2Nat.inj_add.
-    apply Nat.add_le_mono_r. apply le_0_n. discriminate.
-    apply Qplus_lt_l.
-    apply Z.mul_lt_mono_pos_r. simpl. apply Pos2Z.is_pos.
-    reflexivity.
+  apply (Qlt_trans _ (-(2 # k) - xn (n + k)%positive)).
+  specialize (H (n + k)%positive).
+  unfold Qminus in H. rewrite Qplus_0_l in H. apply Qlt_minus_iff in H.
+  unfold Qminus. rewrite Qplus_comm. apply H. apply Pos2Nat.inj_le.
+  rewrite <- (plus_0_l (Pos.to_nat k)). rewrite Pos2Nat.inj_add.
+  apply Nat.add_le_mono_r. apply le_0_n.
+  apply Qplus_lt_l.
+  apply Z.mul_lt_mono_pos_r. simpl. apply Pos2Z.is_pos.
+  reflexivity.
 Qed.
 
 Definition CRealPosShift (x : CReal)
   : inject_Q 0 < x
-    -> { y : prod positive CReal | CRealEq x (snd y)
-                                   /\ forall n:nat, Qlt (1 # fst y) (proj1_sig (snd y) n) }.
+    -> { y : prod positive CReal
+      | x == (snd y) /\ forall n:positive, Qlt (1 # fst y) (proj1_sig (snd y) n) }.
 Proof.
   intro xPos.
   pose proof (CRealLt_aboveSig (inject_Q 0) x).
@@ -943,66 +914,57 @@ Proof.
   pose proof (CRealShiftEqual x).
   destruct xPos as [n maj], x as [xn cau]; simpl in maj.
   simpl in H. specialize (H n).
-  destruct (Qarchimedean (/ (xn (Pos.to_nat n) - 0 - (2 # n)))) as [a _].
+  destruct (Qarchimedean (/ (xn n - 0 - (2 # n)))) as [a _].
   specialize (H maj); simpl in H.
   remember (Pos.max n a~0) as k.
   clear Heqk. clear maj. clear n.
-  exists (pair k
-               (exist _ (fun n => xn (plus n (Pos.to_nat k))) (H0 (Pos.to_nat k)))).
+  exists (pair k (exist _ (fun n => xn (Pos.add n k)) (H0 k))).
   split. apply H1. intro n. simpl. apply Qlt_minus_iff.
-  destruct n.
-  - specialize (H k).
-    unfold Qminus in H. rewrite Qplus_0_r in H.
-    simpl. rewrite <- Qlt_minus_iff.
-    apply (Qlt_trans _ (2 #k)).
-    apply Z.mul_lt_mono_pos_r. simpl. apply Pos2Z.is_pos.
-    reflexivity. apply H. apply Pos.le_refl.
-  - rewrite <- Qlt_minus_iff. apply (Qlt_trans _ (2 # k)).
-    apply Z.mul_lt_mono_pos_r. simpl. apply Pos2Z.is_pos.
-    reflexivity. specialize (H (Pos.of_nat (S n) + k)%positive).
-    unfold Qminus in H. rewrite Qplus_0_r in H.
-    rewrite Pos2Nat.inj_add in H. rewrite Nat2Pos.id in H.
-    apply H. apply Pos2Nat.inj_le.
-    rewrite <- (plus_0_l (Pos.to_nat k)). rewrite Pos2Nat.inj_add.
-    apply Nat.add_le_mono_r. apply le_0_n. discriminate.
+  rewrite <- Qlt_minus_iff. apply (Qlt_trans _ (2 # k)).
+  apply Z.mul_lt_mono_pos_r. simpl. apply Pos2Z.is_pos.
+  reflexivity. specialize (H (n + k)%positive).
+  unfold Qminus in H. rewrite Qplus_0_r in H.
+  apply H. apply Pos2Nat.inj_le.
+  rewrite <- (plus_0_l (Pos.to_nat k)). rewrite Pos2Nat.inj_add.
+  apply Nat.add_le_mono_r. apply le_0_n.
 Qed.
 
-Lemma CReal_inv_neg : forall (yn : nat -> Q) (k : positive),
-    (QCauchySeq yn Pos.to_nat)
-    -> (forall n : nat, yn n < -1 # k)%Q
-    -> QCauchySeq (fun n : nat => / yn (Pos.to_nat k ^ 2 * n)%nat) Pos.to_nat.
+Lemma CReal_inv_neg : forall (yn : positive -> Q) (k : positive),
+    (QCauchySeq yn id)
+    -> (forall n : positive, yn n < -1 # k)%Q
+    -> QCauchySeq (fun n : positive => / yn (k ^ 2 * n)%positive) id.
 Proof.
   (* Prove the inverse sequence is Cauchy *)
   intros yn k cau maj n p q H0 H1.
-  setoid_replace (/ yn (Pos.to_nat k ^ 2 * p)%nat -
-                  / yn (Pos.to_nat k ^ 2 * q)%nat)%Q
-    with ((yn (Pos.to_nat k ^ 2 * q)%nat -
-           yn (Pos.to_nat k ^ 2 * p)%nat)
-            / (yn (Pos.to_nat k ^ 2 * q)%nat *
-               yn (Pos.to_nat k ^ 2 * p)%nat)).
-  + apply (Qle_lt_trans _ (Qabs (yn (Pos.to_nat k ^ 2 * q)%nat
-                                 - yn (Pos.to_nat k ^ 2 * p)%nat)
+  setoid_replace (/ yn (k ^ 2 * p)%positive -
+                  / yn (k ^ 2 * q)%positive)%Q
+    with ((yn (k ^ 2 * q)%positive -
+           yn (k ^ 2 * p)%positive)
+            / (yn (k ^ 2 * q)%positive *
+               yn (k ^ 2 * p)%positive)).
+  + apply (Qle_lt_trans _ (Qabs (yn (k ^ 2 * q)%positive
+                                 - yn (k ^ 2 * p)%positive)
                                 / (1 # (k^2)))).
     assert (1 # k ^ 2
-            < Qabs (yn (Pos.to_nat k ^ 2 * q)%nat * yn (Pos.to_nat k ^ 2 * p)%nat))%Q.
+            < Qabs (yn (k ^ 2 * q)%positive * yn (k ^ 2 * p)%positive))%Q.
     { rewrite Qabs_Qmult. unfold "^"%positive; simpl.
       rewrite factorDenom. rewrite Pos.mul_1_r.
-      apply (Qlt_trans _ ((1#k) * Qabs (yn (Pos.to_nat k * (Pos.to_nat k * 1) * p)%nat))).
+      apply (Qlt_trans _ ((1#k) * Qabs (yn (k * (k * 1) * p)%positive))).
       apply Qmult_lt_l. reflexivity. rewrite Qabs_neg.
-      specialize (maj (Pos.to_nat k * (Pos.to_nat k * 1) * p)%nat).
+      specialize (maj (k * (k * 1) * p)%positive).
       apply Qlt_minus_iff in maj. apply Qlt_minus_iff.
       rewrite Qplus_comm. setoid_replace (-(1#k))%Q with (-1 # k)%Q. apply maj.
       reflexivity. apply (Qle_trans _ (-1 # k)). apply Zlt_le_weak.
-      apply maj. discriminate.
+      apply maj. discriminate. rewrite Pos.mul_1_r.
       apply Qmult_lt_r. apply (Qlt_trans 0 (1#k)). reflexivity.
       rewrite Qabs_neg.
-      specialize (maj (Pos.to_nat k * (Pos.to_nat k * 1) * p)%nat).
+      specialize (maj (k * k * p)%positive).
       apply Qlt_minus_iff in maj. apply Qlt_minus_iff.
-      rewrite Qplus_comm. setoid_replace (-(1#k))%Q with (-1 # k)%Q. apply maj.
-      reflexivity. apply (Qle_trans _ (-1 # k)). apply Zlt_le_weak.
+      rewrite Qplus_comm. setoid_replace (-(1#k))%Q with (-1 # k)%Q.
+      apply maj. reflexivity. apply (Qle_trans _ (-1 # k)). apply Zlt_le_weak.
       apply maj. discriminate.
       rewrite Qabs_neg.
-      specialize (maj (Pos.to_nat k * (Pos.to_nat k * 1) * q)%nat).
+      specialize (maj (k * k * q)%positive).
       apply Qlt_minus_iff in maj. apply Qlt_minus_iff.
       rewrite Qplus_comm. setoid_replace (-(1#k))%Q with (-1 # k)%Q. apply maj.
       reflexivity. apply (Qle_trans _ (-1 # k)). apply Zlt_le_weak.
@@ -1016,66 +978,56 @@ Proof.
     reflexivity. rewrite Qmult_1_l. apply H.
     apply Qabs_nonneg. simpl in maj.
     specialize (cau (n * (k^2))%positive
-                    (Pos.to_nat k ^ 2 * q)%nat
-                    (Pos.to_nat k ^ 2 * p)%nat).
+                    (k ^ 2 * q)%positive
+                    (k ^ 2 * p)%positive).
     apply Qlt_shift_div_r. reflexivity.
     apply (Qlt_le_trans _ (1 # n * k ^ 2)). apply cau.
-    rewrite Pos2Nat.inj_mul. rewrite mult_comm.
-    unfold "^"%positive. simpl. rewrite Pos2Nat.inj_mul.
-    rewrite <- mult_assoc. rewrite <- mult_assoc.
-    apply Nat.mul_le_mono_nonneg_l. apply le_0_n.
-    rewrite (mult_1_r). rewrite Pos.mul_1_r.
-    apply Nat.mul_le_mono_nonneg_l. apply le_0_n.
-    apply (le_trans _ (q+0)). rewrite plus_0_r. assumption.
-    rewrite plus_0_r. apply le_refl.
-    rewrite Pos2Nat.inj_mul. rewrite mult_comm.
-    unfold "^"%positive; simpl. rewrite Pos2Nat.inj_mul.
-    rewrite <- mult_assoc. rewrite <- mult_assoc.
-    apply Nat.mul_le_mono_nonneg_l. apply le_0_n.
-    rewrite (mult_1_r). rewrite Pos.mul_1_r.
-    apply Nat.mul_le_mono_nonneg_l. apply le_0_n.
-    apply (le_trans _ (p+0)). rewrite plus_0_r. assumption.
-    rewrite plus_0_r. apply le_refl.
+    rewrite Pos.mul_comm.
+    unfold "^"%positive. simpl.
+    unfold id. rewrite Pos.mul_1_r.
+    rewrite <- Pos.mul_le_mono_l. exact H1.
+    unfold id. rewrite Pos.mul_comm.
+    apply Pos.mul_le_mono_l. exact H0.
     rewrite factorDenom. apply Qle_refl.
   + field. split. intro abs.
-    specialize (maj (Pos.to_nat k ^ 2 * p)%nat).
+    specialize (maj (k ^ 2 * p)%positive).
     rewrite abs in maj. inversion maj.
     intro abs.
-    specialize (maj (Pos.to_nat k ^ 2 * q)%nat).
+    specialize (maj (k ^ 2 * q)%positive).
     rewrite abs in maj. inversion maj.
 Qed.
 
-Lemma CReal_inv_pos : forall (yn : nat -> Q) (k : positive),
-    (QCauchySeq yn Pos.to_nat)
-    -> (forall n : nat, 1 # k < yn n)%Q
-    -> QCauchySeq (fun n : nat => / yn (Pos.to_nat k ^ 2 * n)%nat) Pos.to_nat.
+Lemma CReal_inv_pos : forall (yn : positive -> Q) (k : positive),
+    (QCauchySeq yn id)
+    -> (forall n : positive, 1 # k < yn n)%Q
+    -> QCauchySeq (fun n : positive => / yn (k ^ 2 * n)%positive) id.
 Proof.
   intros yn k cau maj n p q H0 H1.
-  setoid_replace (/ yn (Pos.to_nat k ^ 2 * p)%nat -
-                  / yn (Pos.to_nat k ^ 2 * q)%nat)%Q
-    with ((yn (Pos.to_nat k ^ 2 * q)%nat -
-           yn (Pos.to_nat k ^ 2 * p)%nat)
-            / (yn (Pos.to_nat k ^ 2 * q)%nat *
-               yn (Pos.to_nat k ^ 2 * p)%nat)).
-  + apply (Qle_lt_trans _ (Qabs (yn (Pos.to_nat k ^ 2 * q)%nat
-                                 - yn (Pos.to_nat k ^ 2 * p)%nat)
+  setoid_replace (/ yn (k ^ 2 * p)%positive -
+                  / yn (k ^ 2 * q)%positive)%Q
+    with ((yn (k ^ 2 * q)%positive -
+           yn (k ^ 2 * p)%positive)
+            / (yn (k ^ 2 * q)%positive *
+               yn (k ^ 2 * p)%positive)).
+  + apply (Qle_lt_trans _ (Qabs (yn (k ^ 2 * q)%positive
+                                 - yn (k ^ 2 * p)%positive)
                                 / (1 # (k^2)))).
     assert (1 # k ^ 2
-            < Qabs (yn (Pos.to_nat k ^ 2 * q)%nat * yn (Pos.to_nat k ^ 2 * p)%nat))%Q.
+            < Qabs (yn (k ^ 2 * q)%positive * yn (k ^ 2 * p)%positive))%Q.
     { rewrite Qabs_Qmult. unfold "^"%positive; simpl.
       rewrite factorDenom. rewrite Pos.mul_1_r.
-      apply (Qlt_trans _ ((1#k) * Qabs (yn (Pos.to_nat k * (Pos.to_nat k * 1) * p)%nat))).
+      apply (Qlt_trans _ ((1#k) * Qabs (yn (k * k * p)%positive))).
       apply Qmult_lt_l. reflexivity. rewrite Qabs_pos.
-      specialize (maj (Pos.to_nat k * (Pos.to_nat k * 1) * p)%nat).
+      specialize (maj (k * k * p)%positive).
       apply maj. apply (Qle_trans _ (1 # k)).
       discriminate. apply Zlt_le_weak. apply maj.
       apply Qmult_lt_r. apply (Qlt_trans 0 (1#k)). reflexivity.
       rewrite Qabs_pos.
-      specialize (maj (Pos.to_nat k * (Pos.to_nat k * 1) * p)%nat).
+      specialize (maj (k * k * p)%positive).
       apply maj. apply (Qle_trans _ (1 # k)). discriminate.
       apply Zlt_le_weak. apply maj.
       rewrite Qabs_pos.
-      specialize (maj (Pos.to_nat k * (Pos.to_nat k * 1) * q)%nat).
+      specialize (maj (k * k * q)%positive).
       apply maj. apply (Qle_trans _ (1 # k)). discriminate.
       apply Zlt_le_weak. apply maj. }
     unfold Qdiv. rewrite Qabs_Qmult. rewrite Qabs_Qinv.
@@ -1087,32 +1039,20 @@ Proof.
     reflexivity. rewrite Qmult_1_l. apply H.
     apply Qabs_nonneg. simpl in maj.
     specialize (cau (n * (k^2))%positive
-                    (Pos.to_nat k ^ 2 * q)%nat
-                    (Pos.to_nat k ^ 2 * p)%nat).
+                    (k ^ 2 * q)%positive
+                    (k ^ 2 * p)%positive).
     apply Qlt_shift_div_r. reflexivity.
     apply (Qlt_le_trans _ (1 # n * k ^ 2)). apply cau.
-    rewrite Pos2Nat.inj_mul. rewrite mult_comm.
-    unfold "^"%positive. simpl. rewrite Pos2Nat.inj_mul.
-    rewrite <- mult_assoc. rewrite <- mult_assoc.
-    apply Nat.mul_le_mono_nonneg_l. apply le_0_n.
-    rewrite (mult_1_r). rewrite Pos.mul_1_r.
-    apply Nat.mul_le_mono_nonneg_l. apply le_0_n.
-    apply (le_trans _ (q+0)). rewrite plus_0_r. assumption.
-    rewrite plus_0_r. apply le_refl.
-    rewrite Pos2Nat.inj_mul. rewrite mult_comm.
-    unfold "^"%positive; simpl. rewrite Pos2Nat.inj_mul.
-    rewrite <- mult_assoc. rewrite <- mult_assoc.
-    apply Nat.mul_le_mono_nonneg_l. apply le_0_n.
-    rewrite (mult_1_r). rewrite Pos.mul_1_r.
-    apply Nat.mul_le_mono_nonneg_l. apply le_0_n.
-    apply (le_trans _ (p+0)). rewrite plus_0_r. assumption.
-    rewrite plus_0_r. apply le_refl.
+    rewrite Pos.mul_comm. unfold id.
+    apply Pos.mul_le_mono_l. exact H1.
+    unfold id. rewrite Pos.mul_comm.
+    apply Pos.mul_le_mono_l. exact H0.
     rewrite factorDenom. apply Qle_refl.
   + field. split. intro abs.
-    specialize (maj (Pos.to_nat k ^ 2 * p)%nat).
+    specialize (maj (k ^ 2 * p)%positive).
     rewrite abs in maj. inversion maj.
     intro abs.
-    specialize (maj (Pos.to_nat k ^ 2 * q)%nat).
+    specialize (maj (k ^ 2 * q)%positive).
     rewrite abs in maj. inversion maj.
 Qed.
 
@@ -1121,11 +1061,11 @@ Proof.
   destruct xnz as [xNeg | xPos].
   - destruct (CRealNegShift x xNeg) as [[k y] [_ maj]].
     destruct y as [yn cau]; unfold proj1_sig, snd, fst in maj.
-    exists (fun n => Qinv (yn (mult (Pos.to_nat k^2) n))).
+    exists (fun n:positive => Qinv (yn (Pos.mul (k^2) n)%positive)).
     apply (CReal_inv_neg yn). apply cau. apply maj.
   - destruct (CRealPosShift x xPos) as [[k y] [_ maj]].
     destruct y as [yn cau]; unfold proj1_sig, snd, fst in maj.
-    exists (fun n => Qinv (yn (mult (Pos.to_nat k^2) n))).
+    exists (fun n => Qinv (yn (Pos.mul (k^2) n))).
     apply (CReal_inv_pos yn). apply cau. apply maj.
 Defined.
 
@@ -1141,19 +1081,20 @@ Proof.
   - destruct (CRealPosShift r c) as [[k rpos] [req maj]].
     clear req. destruct rpos as [rn cau]; simpl in maj.
     unfold CRealLt; simpl.
-    destruct (Qarchimedean (rn 1%nat)) as [A majA].
+    destruct (Qarchimedean (rn 1%positive)) as [A majA].
     exists (2 * (A + 1))%positive. unfold Qminus. rewrite Qplus_0_r.
-    rewrite <- (Qmult_1_l (Qinv (rn (Pos.to_nat k * (Pos.to_nat k * 1) * Pos.to_nat (2 * (A + 1)))%nat))).
+    rewrite <- (Qmult_1_l (Qinv (rn (k * (k * 1) * (2 * (A + 1)))%positive))).
     apply Qlt_shift_div_l. apply (Qlt_trans 0 (1#k)). reflexivity.
     apply maj. rewrite <- (Qmult_inv_r (Z.pos A + 1 # 1)).
     setoid_replace (2 # 2 * (A + 1))%Q with (Qinv (Z.pos A + 1 # 1)).
     2: reflexivity.
     rewrite Qmult_comm. apply Qmult_lt_r. reflexivity.
-    rewrite mult_1_r. rewrite <- Pos2Nat.inj_mul. rewrite <- Pos2Nat.inj_mul.
-    rewrite <- (Qplus_lt_l _ _ (- rn 1%nat)).
-    apply (Qle_lt_trans _ (Qabs (rn (Pos.to_nat (k * k * (2 * (A + 1)))) + - rn 1%nat))).
+    rewrite Pos.mul_1_r.
+    rewrite <- (Qplus_lt_l _ _ (- rn 1%positive)).
+    apply (Qle_lt_trans _ (Qabs (rn (k * k * (2 * (A + 1)))%positive + - rn 1%positive))).
     apply Qle_Qabs. apply (Qlt_le_trans _ 1). apply cau.
-    apply Pos2Nat.is_pos. apply le_refl.
+    destruct (k * k * (2 * (A + 1)))%positive; discriminate.
+    apply Pos.le_refl.
     rewrite <- Qinv_plus_distr. rewrite <- (Qplus_comm 1).
     rewrite <- Qplus_0_r. rewrite <- Qplus_assoc. rewrite <- Qplus_assoc.
     rewrite Qplus_le_r. rewrite Qplus_0_l. apply Qlt_le_weak.
@@ -1161,32 +1102,30 @@ Proof.
     intro abs. inversion abs.
 Qed.
 
-Lemma CReal_linear_shift : forall (x : CReal) (k : nat),
-    le 1 k -> QCauchySeq (fun n => proj1_sig x (k * n)%nat) Pos.to_nat.
-Proof.
-  intros [xn limx] k lek p n m H H0. unfold proj1_sig.
-  apply limx. apply (le_trans _ n). apply H.
-  rewrite <- (mult_1_l n). rewrite mult_assoc.
-  apply Nat.mul_le_mono_nonneg_r. apply le_0_n.
-  rewrite mult_1_r. apply lek. apply (le_trans _ m). apply H0.
-  rewrite <- (mult_1_l m). rewrite mult_assoc.
-  apply Nat.mul_le_mono_nonneg_r. apply le_0_n.
-  rewrite mult_1_r. apply lek.
+Lemma CReal_linear_shift : forall (x : CReal) (k : positive),
+    QCauchySeq (fun n => proj1_sig x (k * n)%positive) id.
+Proof.
+  intros [xn limx] k p n m H H0. unfold proj1_sig.
+  apply limx. apply (Pos.le_trans _ n). apply H.
+  rewrite <- (Pos.mul_1_l n). rewrite Pos.mul_assoc.
+  apply Pos.mul_le_mono_r. destruct (k*1)%positive; discriminate.
+  apply (Pos.le_trans _ (1*m)). exact H0.
+  apply Pos.mul_le_mono_r. destruct k; discriminate.
 Qed.
 
-Lemma CReal_linear_shift_eq : forall (x : CReal) (k : nat) (kPos : le 1 k),
+Lemma CReal_linear_shift_eq : forall (x : CReal) (k : positive),
     CRealEq x
-    (exist (fun n : nat -> Q => QCauchySeq n Pos.to_nat)
-           (fun n : nat => proj1_sig x (k * n)%nat) (CReal_linear_shift x k kPos)).
+    (exist (fun n : positive -> Q => QCauchySeq n id)
+           (fun n : positive => proj1_sig x (k * n)%positive) (CReal_linear_shift x k)).
 Proof.
   intros. apply CRealEq_diff. intro n.
   destruct x as [xn limx]; unfold proj1_sig.
-  specialize (limx n (Pos.to_nat n) (k * Pos.to_nat n)%nat).
+  specialize (limx n n (k * n)%positive).
   apply (Qle_trans _ (1 # n)). apply Qlt_le_weak. apply limx.
-  apply le_refl. rewrite <- (mult_1_l (Pos.to_nat n)).
-  rewrite mult_assoc. apply Nat.mul_le_mono_nonneg_r. apply le_0_n.
-  rewrite mult_1_r. apply kPos. apply Z.mul_le_mono_nonneg_r.
-  discriminate. discriminate.
+  apply Pos.le_refl. rewrite <- (Pos.mul_1_l n).
+  rewrite Pos.mul_assoc. apply Pos.mul_le_mono_r.
+  destruct (k*1)%positive; discriminate.
+  apply Z.mul_le_mono_nonneg_r. discriminate. discriminate.
 Qed.
 
 Lemma CReal_inv_l : forall (r:CReal) (rnz : r # 0),
@@ -1199,57 +1138,55 @@ Proof.
     apply (QSeqEquivEx_trans _
              (proj1_sig (CReal_mult ((let
               (yn, cau) as s
-               return ((forall n : nat, proj1_sig s n < -1 # k) -> CReal) := rneg in
-            fun maj0 : forall n : nat, yn n < -1 # k =>
-            exist (fun x : nat -> Q => QCauchySeq x Pos.to_nat)
-              (fun n : nat => Qinv (yn (Pos.to_nat k * (Pos.to_nat k * 1) * n))%nat)
+               return ((forall n : positive, proj1_sig s n < -1 # k) -> CReal) := rneg in
+            fun maj0 : forall n : positive, yn n < -1 # k =>
+            exist (fun x : positive -> Q => QCauchySeq x id)
+              (fun n : positive => Qinv (yn (k * (k * 1) * n))%positive)
               (CReal_inv_neg yn k cau maj0)) maj) rneg)))%Q.
     + apply CRealEq_modindep. apply CRealEq_diff.
       apply CReal_mult_proper_l. apply req.
-    + assert (le 1 (Pos.to_nat k * (Pos.to_nat k * 1))%nat). rewrite mult_1_r.
-      rewrite <- Pos2Nat.inj_mul. apply Pos2Nat.is_pos.
-      apply (QSeqEquivEx_trans _
+    + apply (QSeqEquivEx_trans _
              (proj1_sig (CReal_mult ((let
               (yn, cau) as s
-               return ((forall n : nat, proj1_sig s n < -1 # k) -> CReal) := rneg in
-            fun maj0 : forall n : nat, yn n < -1 # k =>
-            exist (fun x : nat -> Q => QCauchySeq x Pos.to_nat)
-              (fun n : nat => Qinv (yn (Pos.to_nat k * (Pos.to_nat k * 1) * n)%nat))
+               return ((forall n : positive, proj1_sig s n < -1 # k) -> CReal) := rneg in
+            fun maj0 : forall n : positive, yn n < -1 # k =>
+            exist (fun x : positive -> Q => QCauchySeq x id)
+              (fun n : positive => Qinv (yn (k * (k * 1) * n)%positive))
               (CReal_inv_neg yn k cau maj0)) maj)
-                                    (exist _ (fun n => proj1_sig rneg (Pos.to_nat k * (Pos.to_nat k * 1) * n)%nat) (CReal_linear_shift rneg _ H)))))%Q.
+                                    (exist _ (fun n => proj1_sig rneg (k * (k * 1) * n)%positive) (CReal_linear_shift rneg _)))))%Q.
       apply CRealEq_modindep. apply CRealEq_diff.
       apply CReal_mult_proper_l. apply CReal_linear_shift_eq.
       destruct r as [rn limr], rneg as [rnn limneg]; simpl.
       pose proof (QCauchySeq_bounded_prop
-                  (fun n : nat => Qinv (rnn (Pos.to_nat k * (Pos.to_nat k * 1) * n)%nat))
-                  Pos.to_nat (CReal_inv_neg rnn k limneg maj)).
+                  (fun n : positive => Qinv (rnn (k * (k * 1) * n)%positive))
+                  id (CReal_inv_neg rnn k limneg maj)).
       pose proof (QCauchySeq_bounded_prop
-            (fun n : nat => rnn (Pos.to_nat k * (Pos.to_nat k * 1) * n)%nat)
-            Pos.to_nat
+            (fun n : positive => rnn (k * (k * 1) * n)%positive)
+            id
             (CReal_linear_shift
-               (exist (fun x0 : nat -> Q => QCauchySeq x0 Pos.to_nat) rnn limneg)
-               (Pos.to_nat k * (Pos.to_nat k * 1)) H)) ; simpl.
+               (exist (fun x0 : positive -> Q => QCauchySeq x0 id) rnn limneg)
+               (k * (k * 1)))) ; simpl.
       remember (QCauchySeq_bound
-             (fun n0 : nat => / rnn (Pos.to_nat k * (Pos.to_nat k * 1) * n0)%nat)%Q
-             Pos.to_nat) as x.
+             (fun n0 : positive => / rnn (k * (k * 1) * n0)%positive)%Q
+             id) as x.
       remember (QCauchySeq_bound
-             (fun n0 : nat => rnn (Pos.to_nat k * (Pos.to_nat k * 1) * n0)%nat)
-             Pos.to_nat) as x0.
-      exists (fun n => 1%nat). intros p n m H2 H3. rewrite Qmult_comm.
+             (fun n0 : positive => rnn (k * (k * 1) * n0)%positive)
+             id) as x0.
+      exists (fun n => 1%positive). intros p n m H2 H3. rewrite Qmult_comm.
       rewrite Qmult_inv_r. unfold Qminus. rewrite Qplus_opp_r.
       reflexivity. intro abs.
-      specialize (maj (Pos.to_nat k * (Pos.to_nat k * 1)
-                       * (Pos.to_nat (Pos.max x x0)~0 * n))%nat).
-      simpl in maj. rewrite abs in maj. inversion maj.
+      unfold snd,fst, proj1_sig in maj.
+      specialize (maj (k * (k * 1) * (Pos.max x x0 * n)~0)%positive).
+      rewrite abs in maj. inversion maj.
   - (* r > 0 *) destruct (CRealPosShift r c) as [[k rneg] [req maj]].
     simpl in req. apply CRealEq_diff. apply CRealEq_modindep.
     apply (QSeqEquivEx_trans _
              (proj1_sig (CReal_mult ((let
               (yn, cau) as s
-               return ((forall n : nat, 1 # k < proj1_sig s n) -> CReal) := rneg in
-            fun maj0 : forall n : nat, 1 # k < yn n =>
-            exist (fun x : nat -> Q => QCauchySeq x Pos.to_nat)
-              (fun n : nat => Qinv (yn (Pos.to_nat k * (Pos.to_nat k * 1) * n)%nat))
+               return ((forall n : positive, 1 # k < proj1_sig s n) -> CReal) := rneg in
+            fun maj0 : forall n : positive, 1 # k < yn n =>
+            exist (fun x : positive -> Q => QCauchySeq x id)
+              (fun n : positive => Qinv (yn (k * (k * 1) * n)%positive))
               (CReal_inv_pos yn k cau maj0)) maj) rneg)))%Q.
     + apply CRealEq_modindep. apply CRealEq_diff.
       apply CReal_mult_proper_l. apply req.
@@ -1258,35 +1195,34 @@ Proof.
       apply (QSeqEquivEx_trans _
              (proj1_sig (CReal_mult ((let
               (yn, cau) as s
-               return ((forall n : nat, 1 # k < proj1_sig s n) -> CReal) := rneg in
-            fun maj0 : forall n : nat, 1 # k < yn n =>
-            exist (fun x : nat -> Q => QCauchySeq x Pos.to_nat)
-              (fun n : nat => Qinv (yn (Pos.to_nat k * (Pos.to_nat k * 1) * n)%nat))
+               return ((forall n : positive, 1 # k < proj1_sig s n) -> CReal) := rneg in
+            fun maj0 : forall n : positive, 1 # k < yn n =>
+            exist (fun x : positive -> Q => QCauchySeq x id)
+              (fun n : positive => Qinv (yn (k * (k * 1) * n)%positive))
               (CReal_inv_pos yn k cau maj0)) maj)
-                                    (exist _ (fun n => proj1_sig rneg (Pos.to_nat k * (Pos.to_nat k * 1) * n)%nat) (CReal_linear_shift rneg _ H)))))%Q.
+                                    (exist _ (fun n => proj1_sig rneg (k * (k * 1) * n)%positive) (CReal_linear_shift rneg _)))))%Q.
       apply CRealEq_modindep. apply CRealEq_diff.
       apply CReal_mult_proper_l. apply CReal_linear_shift_eq.
       destruct r as [rn limr], rneg as [rnn limneg]; simpl.
       pose proof (QCauchySeq_bounded_prop
-                  (fun n : nat => Qinv (rnn (Pos.to_nat k * (Pos.to_nat k * 1) * n)%nat))
-                  Pos.to_nat (CReal_inv_pos rnn k limneg maj)).
+                  (fun n : positive => Qinv (rnn (k * (k * 1) * n)%positive))
+                  id (CReal_inv_pos rnn k limneg maj)).
       pose proof (QCauchySeq_bounded_prop
-            (fun n : nat => rnn (Pos.to_nat k * (Pos.to_nat k * 1) * n)%nat)
-            Pos.to_nat
+            (fun n : positive => rnn (k * (k * 1) * n)%positive)
+            id
             (CReal_linear_shift
-               (exist (fun x0 : nat -> Q => QCauchySeq x0 Pos.to_nat) rnn limneg)
-               (Pos.to_nat k * (Pos.to_nat k * 1)) H)) ; simpl.
+               (exist (fun x0 : positive -> Q => QCauchySeq x0 id) rnn limneg)
+               (k * (k * 1)))) ; simpl.
       remember (QCauchySeq_bound
-             (fun n0 : nat => / rnn (Pos.to_nat k * (Pos.to_nat k * 1) * n0)%nat)
-             Pos.to_nat)%Q as x.
+             (fun n0 : positive => / rnn (k * (k * 1) * n0)%positive)
+             id)%Q as x.
       remember (QCauchySeq_bound
-             (fun n0 : nat => rnn (Pos.to_nat k * (Pos.to_nat k * 1) * n0)%nat)
-             Pos.to_nat) as x0.
-      exists (fun n => 1%nat). intros p n m H2 H3. rewrite Qmult_comm.
+             (fun n0 : positive => rnn (k * (k * 1) * n0)%positive)
+             id) as x0.
+      exists (fun n => 1%positive). intros p n m H2 H3. rewrite Qmult_comm.
       rewrite Qmult_inv_r. unfold Qminus. rewrite Qplus_opp_r.
       reflexivity. intro abs.
-      specialize (maj (Pos.to_nat k * (Pos.to_nat k * 1)
-                       * (Pos.to_nat (Pos.max x x0)~0 * n))%nat).
+      specialize (maj ((k * (k * 1) * (Pos.max x x0 * n)~0)%positive)).
       simpl in maj. rewrite abs in maj. inversion maj.
 Qed.
 
@@ -1369,12 +1305,13 @@ Proof.
   apply CRealLt_above in c. destruct c as [i imaj]. simpl in imaj.
   apply CRealLt_above in c0. destruct c0 as [j jmaj]. simpl in jmaj.
   pose proof (CReal_abs_appart_zero y).
-  destruct x as [xn xcau], y as [yn ycau]. simpl in kmaj.
-  remember (QCauchySeq_bound xn Pos.to_nat) as a.
-  remember (QCauchySeq_bound yn Pos.to_nat) as b.
-  simpl in kmaj. simpl in imaj, jmaj. simpl in H0.
+  destruct x as [xn xcau], y as [yn ycau].
+  unfold CReal_mult, proj1_sig in kmaj.
+  remember (QCauchySeq_bound xn id) as a.
+  remember (QCauchySeq_bound yn id) as b.
+  simpl in imaj, jmaj. simpl in H0.
   specialize (kmaj (Pos.max k (Pos.max i j)) (Pos.le_max_l _ _)).
-  destruct (H0 ((Pos.max a b)~0 * (Pos.max k (Pos.max i j)))%positive).
+  destruct (H0 (2*(Pos.max a b) * (Pos.max k (Pos.max i j)))%positive).
   - apply (Qlt_trans _ (2#k)).
     + unfold Qlt. rewrite <- Z.mul_lt_mono_pos_l. 2: reflexivity.
       unfold Qden. apply Pos2Z.pos_lt_pos.
@@ -1385,11 +1322,8 @@ Proof.
       fold (2*Pos.max a b)%positive. rewrite Pos2Nat.inj_mul.
       apply Nat.lt_1_mul_pos. auto. apply Pos2Nat.is_pos.
     + apply (Qlt_le_trans _ _ _ kmaj). unfold Qminus. rewrite Qplus_0_r.
-      rewrite <- (Qmult_1_l (Qabs (yn (Pos.to_nat ((Pos.max a b)~0 * Pos.max k (Pos.max i j)))))).
+      rewrite <- (Qmult_1_l (Qabs (yn (2*(Pos.max a b) * Pos.max k (Pos.max i j))%positive))).
       apply (Qle_trans _ _ _ (Qle_Qabs _)). rewrite Qabs_Qmult.
-      replace (Pos.to_nat (Pos.max a b)~0 * Pos.to_nat (Pos.max k (Pos.max i j)))%nat
-        with (Pos.to_nat ((Pos.max a b)~0 * Pos.max k (Pos.max i j))).
-      2: apply Pos2Nat.inj_mul.
       apply Qmult_le_compat_r. 2: apply Qabs_nonneg.
       apply Qabs_Qle_condition. split.
       apply Qlt_le_weak. apply Qlt_minus_iff, (Qlt_trans _ (2#j)).
@@ -1398,18 +1332,14 @@ Proof.
       rewrite Pos.mul_1_l.
       apply (Pos.le_trans _ (Pos.max i j) _ (Pos.le_max_r _ _)).
       apply Pos.le_max_r.
-      apply Pos2Nat.inj_le. do 2 rewrite Pos2Nat.inj_mul.
-      rewrite <- Nat.mul_le_mono_pos_r. 2: apply Pos2Nat.is_pos.
-      apply Pos2Nat.is_pos.
+      rewrite <- Pos.mul_le_mono_r. discriminate.
       apply Qlt_le_weak. apply Qlt_minus_iff, (Qlt_trans _ (2#i)).
       reflexivity. apply imaj.
       apply (Pos.le_trans _ (1 * Pos.max k (Pos.max i j))).
       rewrite Pos.mul_1_l.
       apply (Pos.le_trans _ (Pos.max i j) _ (Pos.le_max_l _ _)).
       apply Pos.le_max_r.
-      apply Pos2Nat.inj_le. do 2 rewrite Pos2Nat.inj_mul.
-      rewrite <- Nat.mul_le_mono_pos_r. 2: apply Pos2Nat.is_pos.
-      apply Pos2Nat.is_pos.
+      rewrite <- Pos.mul_le_mono_r. discriminate.
   - left. apply (CReal_mult_lt_reg_r (exist _ yn ycau) _ _ c).
     rewrite CReal_mult_0_l. exact H.
   - right. apply (CReal_mult_lt_reg_r (CReal_opp (exist _ yn ycau))).
@@ -1450,11 +1380,11 @@ Proof.
   (* Locate a and b at the index given by a<b,
      and pick the middle rational number. *)
   intros [p pmaj].
-  exists ((proj1_sig a (Pos.to_nat p) + proj1_sig b (Pos.to_nat p)) * (1#2))%Q.
+  exists ((proj1_sig a p + proj1_sig b p) * (1#2))%Q.
   split.
   - apply (CReal_le_lt_trans _ _ _ (inject_Q_compare a p)). apply inject_Q_lt.
     apply (Qmult_lt_l _ _ 2). reflexivity.
-    apply (Qplus_lt_l _ _ (-2*proj1_sig a (Pos.to_nat p))).
+    apply (Qplus_lt_l _ _ (-2*proj1_sig a p)).
     field_simplify. field_simplify in pmaj.
     setoid_replace (-2#2)%Q with (-1)%Q. 2: reflexivity.
     setoid_replace (2*(1#p))%Q with (2#p)%Q. 2: reflexivity.
@@ -1462,12 +1392,12 @@ Proof.
   - apply (CReal_plus_lt_reg_l (-b)).
     rewrite CReal_plus_opp_l.
     apply (CReal_plus_lt_reg_r
-             (-inject_Q ((proj1_sig a (Pos.to_nat p) + proj1_sig b (Pos.to_nat p)) * (1 # 2)))).
+             (-inject_Q ((proj1_sig a p + proj1_sig b p) * (1 # 2)))).
     rewrite CReal_plus_assoc, CReal_plus_opp_r, CReal_plus_0_r, CReal_plus_0_l.
     rewrite <- opp_inject_Q.
     apply (CReal_le_lt_trans _ _ _ (inject_Q_compare (-b) p)). apply inject_Q_lt.
     apply (Qmult_lt_l _ _ 2). reflexivity.
-    apply (Qplus_lt_l _ _ (2*proj1_sig b (Pos.to_nat p))).
+    apply (Qplus_lt_l _ _ (2*proj1_sig b p)).
     destruct b as [bn bcau]; simpl. simpl in pmaj.
     field_simplify. field_simplify in pmaj.
     setoid_replace (-2#2)%Q with (-1)%Q. 2: reflexivity.
diff --git a/theories/Reals/Cauchy/ConstructiveRcomplete.v b/theories/Reals/Cauchy/ConstructiveRcomplete.v
index 51fd0dd7f9..6f36e888ed 100644
--- a/theories/Reals/Cauchy/ConstructiveRcomplete.v
+++ b/theories/Reals/Cauchy/ConstructiveRcomplete.v
@@ -47,44 +47,6 @@ Proof.
   intros. apply (seq_cv_proper un y). exact H0. symmetry. exact H.
 Qed.
 
-Lemma growing_transit : forall un : nat -> CReal,
-    (forall n:nat, un n <= un (S n))
-    -> forall n p : nat, le n p -> un n <= un p.
-Proof.
-  induction p.
-  - intros. inversion H0. apply CRealLe_refl.
-  - intros. apply Nat.le_succ_r in H0. destruct H0.
-    apply (CReal_le_trans _ (un p)). apply IHp, H0. apply H.
-    subst n. apply CRealLe_refl.
-Qed.
-
-Lemma growing_infinite : forall un : nat -> nat,
-    (forall n:nat, lt (un n) (un (S n)))
-    -> forall n : nat, le n (un n).
-Proof.
-  induction n.
-  - apply le_0_n.
-  - specialize (H n). unfold lt in H.
-    apply (le_trans _ (S (un n))). apply le_n_S, IHn. exact H.
-Qed.
-
-Lemma Un_cv_growing : forall (un : nat -> CReal) (l : CReal),
-    (forall n:nat, un n <= un (S n))
-    -> (forall n:nat, un n <= l)
-    -> (forall p : positive, { n : nat  |  l - un n <= inject_Q (1#p) })
-    -> seq_cv un l.
-Proof.
-  intros. intro p.
-  specialize (H1 p) as [n nmaj]. exists n.
-  intros. rewrite CReal_abs_minus_sym, CReal_abs_right.
-  apply (CReal_le_trans _ (l - un n)). apply CReal_plus_le_compat_l.
-  apply CReal_opp_ge_le_contravar.
-  exact (growing_transit _ H n i H1). exact nmaj.
-  rewrite <- (CReal_plus_opp_r (un i)). apply CReal_plus_le_compat.
-  apply H0. apply CRealLe_refl.
-Qed.
-
-
 
 (* Sharpen the archimedean property : constructive versions of
    the usual floor and ceiling functions. *)
@@ -157,15 +119,6 @@ Proof.
     unfold Qeq; simpl. rewrite Pos.mul_1_r, Z.mul_1_r. reflexivity.
 Qed.
 
-Definition RQ_limit : forall (x : CReal) (n:nat),
-    { q:Q  &  x < inject_Q q < x + inject_Q (1 # Pos.of_nat n) }.
-Proof.
-  intros x n. apply (FQ_dense x (x + inject_Q (1 # Pos.of_nat n))).
-  rewrite <- (CReal_plus_0_r x). rewrite CReal_plus_assoc.
-  apply CReal_plus_lt_compat_l. rewrite CReal_plus_0_l. apply inject_Q_lt.
-  reflexivity.
-Qed.
-
 Lemma Qabs_Rabs : forall q : Q,
     inject_Q (Qabs q) == CReal_abs (inject_Q q).
 Proof.
@@ -176,173 +129,86 @@ Proof.
     apply inject_Q_le, H.
 Qed.
 
-Definition Un_cauchy_Q (xn : nat -> Q) : Set
-  := forall n : positive,
-    { k : nat | forall p q : nat, le k p -> le k q
-                                  -> (Qabs (xn p - xn q) <= 1#n)%Q }.
-
-Lemma CReal_smaller_interval : forall a b c d : CReal,
-    a <= c -> c <= b
-    -> a <= d -> d <= b
-    -> CReal_abs (d - c) <= b-a.
-Proof.
-  intros. apply CReal_abs_le. split.
-  - apply (CReal_plus_le_reg_l (b+c)). ring_simplify.
-    apply CReal_plus_le_compat; assumption.
-  - apply (CReal_plus_le_reg_l (a+c)). ring_simplify.
-    apply CReal_plus_le_compat; assumption.
-Qed.
-
-Lemma Rdiag_cauchy_sequence : forall (xn : nat -> CReal),
-    Un_cauchy_mod xn
-    -> Un_cauchy_Q (fun n:nat => let (l,_) := RQ_limit (xn n) n in l).
-Proof.
-  intros xn H p. specialize (H (2 * p)%positive) as [k cv].
-  exists (max k (2 * Pos.to_nat p)). intros.
-  specialize (cv p0 q
-                 (le_trans _ _ _ (Nat.le_max_l _ _) H)
-                 (le_trans _ _ _ (Nat.le_max_l _ _) H0)).
-  destruct (RQ_limit (xn p0) p0) as [r rmaj].
-  destruct (RQ_limit (xn q) q) as [s smaj].
-  apply Qabs_Qle_condition. split.
-  - apply le_inject_Q. unfold Qminus.
-    apply (CReal_le_trans _ (xn p0 - (xn q + inject_Q (1 # 2 * p)))).
-    + unfold CReal_minus. rewrite CReal_opp_plus_distr.
-      rewrite <- CReal_plus_assoc.
-      apply (CReal_plus_le_reg_r (xn q - xn p0 - inject_Q (-(1#p)))).
-      ring_simplify. unfold CReal_minus. do 2 rewrite <- opp_inject_Q.
-      rewrite <- inject_Q_plus.
-      setoid_replace (- - (1 # p) + - (1 # 2 * p))%Q with (1 # 2 * p)%Q.
-      rewrite CReal_abs_minus_sym in cv.
-      exact (CReal_le_trans _ _ _ (CReal_le_abs _ ) cv).
-      rewrite Qopp_involutive.
-      setoid_replace (1#p)%Q with (2 # 2 *p)%Q. rewrite Qinv_minus_distr.
-      reflexivity. reflexivity.
-    + rewrite inject_Q_plus. apply CReal_plus_le_compat.
-      apply CRealLt_asym.
-      destruct (RQ_limit (xn p0) p0); simpl. apply rmaj.
-      apply CRealLt_asym.
-      rewrite opp_inject_Q. apply CReal_opp_gt_lt_contravar.
-      destruct smaj. apply (CReal_lt_le_trans _ _ _ c0).
-      apply CReal_plus_le_compat_l. apply inject_Q_le.
-      apply Z2Nat.inj_le. discriminate. discriminate.
-      simpl. assert ((Pos.to_nat p~0 <= q)%nat).
-      { apply (le_trans _ (Init.Nat.max k (2 * Pos.to_nat p))).
-        2: apply H0. replace (p~0)%positive with (2*p)%positive.
-        2: reflexivity. rewrite Pos2Nat.inj_mul.
-        apply Nat.le_max_r. }
-      rewrite Nat2Pos.id. apply H1. intro abs. subst q.
-      inversion H1. pose proof (Pos2Nat.is_pos (p~0)).
-      rewrite H3 in H2. inversion H2.
-  - apply le_inject_Q. unfold Qminus.
-    apply (CReal_le_trans _ (xn p0 + inject_Q (1 # 2 * p) - xn q)).
-    + rewrite inject_Q_plus. apply CReal_plus_le_compat.
-      apply CRealLt_asym.
-      destruct (RQ_limit (xn p0) p0); unfold proj1_sig.
-      apply (CReal_lt_le_trans _ (xn p0 + inject_Q (1 # Pos.of_nat p0))).
-      apply rmaj. apply CReal_plus_le_compat_l. apply inject_Q_le.
-      apply Z2Nat.inj_le. discriminate. discriminate.
-      simpl. assert ((Pos.to_nat p~0 <= p0)%nat).
-      { apply (le_trans _ (Init.Nat.max k (2 * Pos.to_nat p))).
-        2: apply H. replace (p~0)%positive with (2*p)%positive.
-        2: reflexivity. rewrite Pos2Nat.inj_mul.
-        apply Nat.le_max_r. }
-      rewrite Nat2Pos.id. apply H1. intro abs. subst p0.
-      inversion H1. pose proof (Pos2Nat.is_pos (p~0)).
-      rewrite H3 in H2. inversion H2.
-      apply CRealLt_asym.
-      rewrite opp_inject_Q. apply CReal_opp_gt_lt_contravar.
-      destruct (RQ_limit (xn q) q); simpl. apply smaj.
-    + unfold CReal_minus. rewrite (CReal_plus_comm (xn p0)).
-      rewrite CReal_plus_assoc.
-      apply (CReal_plus_le_reg_l (- inject_Q (1 # 2 * p))).
-      rewrite <- CReal_plus_assoc. rewrite CReal_plus_opp_l. rewrite CReal_plus_0_l.
-      rewrite <- opp_inject_Q. rewrite <- inject_Q_plus.
-      setoid_replace (- (1 # 2 * p) + (1 # p))%Q with (1 # 2 * p)%Q.
-      exact (CReal_le_trans _ _ _ (CReal_le_abs _) cv).
-      rewrite Qplus_comm.
-      setoid_replace (1#p)%Q with (2 # 2*p)%Q. rewrite Qinv_minus_distr.
-      reflexivity. reflexivity.
-Qed.
-
-Lemma CReal_absSmall : forall (x y : CReal) (n : positive),
-    (Qlt (2 # n)
-         (proj1_sig x (Pos.to_nat n) - Qabs (proj1_sig y (Pos.to_nat n))))
-    -> CReal_abs y <= x.
-Proof.
-  intros x y n maj. apply CReal_abs_le. split.
-  - apply CRealLt_asym. exists n. destruct x as [xn caux], y as [yn cauy]; simpl.
-    simpl in maj. unfold Qminus. rewrite Qopp_involutive.
-    rewrite Qplus_comm.
-    apply (Qlt_le_trans _ (xn (Pos.to_nat n) - Qabs (yn (Pos.to_nat n)))).
-    apply maj. apply Qplus_le_r.
-    rewrite <- (Qopp_involutive (yn (Pos.to_nat n))).
-    apply Qopp_le_compat. rewrite Qabs_opp. apply Qle_Qabs.
-  - apply CRealLt_asym. exists n. destruct x as [xn caux], y as [yn cauy]; simpl.
-    simpl in maj.
-    apply (Qlt_le_trans _ (xn (Pos.to_nat n) - Qabs (yn (Pos.to_nat n)))).
-    apply maj. apply Qplus_le_r. apply Qopp_le_compat. apply Qle_Qabs.
-Qed.
-
 
-(* An element of CReal is a Cauchy sequence of rational numbers,
-   show that it converges to itself in CReal. *)
-Lemma CReal_cv_self : forall (qn : nat -> Q) (x : CReal) (cvmod : positive -> nat),
-    QSeqEquiv qn (fun n => proj1_sig x n) cvmod
-    -> seq_cv (fun n => inject_Q (qn n)) x.
+(* For instance the rational sequence 1/n converges to 0. *)
+Lemma CReal_cv_self : forall (x : CReal) (n : positive),
+    CReal_abs (x - inject_Q (proj1_sig x n)) <= inject_Q (1#n).
 Proof.
-  intros qn x cvmod H p.
-  specialize (H (2*p)%positive). exists (cvmod (2*p)%positive).
-  intros p0 H0.
-  apply (CReal_absSmall
-           _ _ (Pos.max (4 * p)%positive (Pos.of_nat (cvmod (2 * p)%positive)))).
-  setoid_replace (proj1_sig (inject_Q (1 # p)) (Pos.to_nat (Pos.max (4 * p) (Pos.of_nat (cvmod (2 * p)%positive)))))
-    with (1 # p)%Q.
-  2: reflexivity.
-  setoid_replace (proj1_sig (CReal_plus (inject_Q (qn p0)) (CReal_opp x)) (Pos.to_nat (Pos.max (4 * p) (Pos.of_nat (cvmod (2 * p)%positive)))))
-    with (qn p0 - proj1_sig x (2 * (Pos.to_nat (Pos.max (4 * p) (Pos.of_nat (cvmod (2 * p)%positive)))))%nat)%Q.
-  2: destruct x; reflexivity.
-  apply (Qle_lt_trans _ (1 # 2 * p)).
-  unfold Qle; simpl. rewrite Pos2Z.inj_max. apply Z.le_max_l.
-  rewrite <- (Qplus_lt_r
-               _ _ (Qabs
-     (qn p0 -
-      proj1_sig x
-                (2 * Pos.to_nat (Pos.max (4 * p) (Pos.of_nat (cvmod (2 * p)%positive))))%nat)
-                    -(1#2*p))).
-  ring_simplify.
-  setoid_replace (-1 * (1 # 2 * p) + (1 # p))%Q with (1 # 2 * p)%Q.
-  apply H. apply H0. rewrite Pos2Nat.inj_max.
-  apply (le_trans _ (1 * Nat.max (Pos.to_nat (4 * p)) (Pos.to_nat (Pos.of_nat (cvmod (2 * p)%positive))))).
-  destruct (cvmod (2*p)%positive). apply le_0_n. rewrite mult_1_l.
-  rewrite Nat2Pos.id. 2: discriminate. apply Nat.le_max_r.
-  apply Nat.mul_le_mono_nonneg_r. apply le_0_n. auto.
-  setoid_replace (1 # p)%Q with (2 # 2 * p)%Q.
-  rewrite Qplus_comm. rewrite Qinv_minus_distr.
-  reflexivity. reflexivity.
+  intros x n [k kmaj].
+  destruct x as [xn cau].
+  unfold CReal_abs, CReal_minus, CReal_plus, CReal_opp, inject_Q, proj1_sig in kmaj.
+  apply (Qlt_not_le _ _ kmaj). clear kmaj.
+  unfold QCauchySeq, QSeqEquiv in cau.
+  rewrite <- (Qplus_le_l _ _ (1#n)). ring_simplify. unfold id in cau.
+  destruct (Pos.lt_total (2*k) n). 2: destruct H.
+  - specialize (cau k (2*k)%positive n).
+    assert (k <= 2 * k)%positive.
+    { apply (Pos.le_trans _ (1*k)). apply Pos.le_refl.
+      apply Pos.mul_le_mono_r. discriminate. }
+    apply (Qle_trans _ (1#k)). apply Qlt_le_weak, cau.
+    exact H0. apply (Pos.le_trans _ _ _ H0). apply Pos.lt_le_incl, H.
+    rewrite <- (Qinv_plus_distr 1 1).
+    apply (Qplus_le_l _ _ (-(1#k))). ring_simplify. discriminate.
+  - subst n. rewrite Qplus_opp_r. discriminate.
+  - specialize (cau n (2*k)%positive n).
+    apply (Qle_trans _ (1#n)). apply Qlt_le_weak, cau.
+    apply Pos.lt_le_incl, H. apply Pos.le_refl.
+    apply (Qplus_le_l _ _ (-(1#n))). ring_simplify. discriminate.
 Qed.
 
-(* Q is dense in Archimedean fields, so all real numbers
-   are limits of rational sequences.
-   The biggest computable such field has all rational limits. *)
-Lemma R_has_all_rational_limits : forall qn : nat -> Q,
-    Un_cauchy_Q qn
-    -> { r : CReal  &  seq_cv (fun n:nat => inject_Q (qn n)) r }.
+(* We can probably reduce the factor 4. *)
+Lemma Rcauchy_limit : forall (xn : nat -> CReal) (xcau : Un_cauchy_mod xn),
+    QCauchySeq
+      (fun n : positive =>
+         let (p, _) := xcau (4 * n)%positive in proj1_sig (xn p) (4 * n)%positive) id.
 Proof.
-  (* qn is an element of CReal. Show that inject_Q qn
-     converges to it in CReal. *)
-  intros.
-  destruct (standard_modulus qn (fun p => proj1_sig (H (Pos.succ p)))).
-  - intros p n k H0 H1. destruct (H (Pos.succ p)%positive) as [x a]; simpl in H0,H1.
-    specialize (a n k H0 H1).
-    apply (Qle_lt_trans _ (1#Pos.succ p) _ a).
-    apply Pos2Z.pos_lt_pos. simpl. apply Pos.lt_succ_diag_r.
-  - exists (exist _ (fun n : nat =>
-                       qn (increasing_modulus (fun p : positive => proj1_sig (H (Pos.succ p))) n)) H0).
-    apply (CReal_cv_self qn (exist _ (fun n : nat =>
-                qn (increasing_modulus (fun p : positive => proj1_sig (H (Pos.succ p))) n)) H0)
-          (fun p : positive => Init.Nat.max (proj1_sig (H (Pos.succ p))) (Pos.to_nat p))).
-    apply H1.
+  intros xn xcau n p q H0 H1.
+  destruct (xcau (4 * p)%positive) as [i imaj],
+  (xcau (4 * q)%positive) as [j jmaj].
+  assert (CReal_abs (xn i - xn j) <= inject_Q (1 # 4 * n)).
+  { destruct (le_lt_dec i j).
+    apply (CReal_le_trans _ _ _ (imaj i j (le_refl _) l)).
+    apply inject_Q_le. unfold Qle, Qnum, Qden.
+    rewrite Z.mul_1_l, Z.mul_1_l. apply Pos2Z.pos_le_pos.
+    apply Pos.mul_le_mono_l, H0. apply le_S, le_S_n in l.
+    apply (CReal_le_trans _ _ _ (jmaj i j l (le_refl _))).
+    apply inject_Q_le. unfold Qle, Qnum, Qden.
+    rewrite Z.mul_1_l, Z.mul_1_l. apply Pos2Z.pos_le_pos.
+    apply Pos.mul_le_mono_l, H1. }
+  clear jmaj imaj.
+  setoid_replace (1#n)%Q with ((1#(3*n)) + ((1#(3*n)) + (1#(3*n))))%Q.
+  2: rewrite Qinv_plus_distr, Qinv_plus_distr; reflexivity.
+  apply lt_inject_Q. rewrite inject_Q_plus.
+  rewrite Qabs_Rabs.
+  apply (CReal_le_lt_trans _ (CReal_abs (inject_Q (proj1_sig (xn i) (4 * p)%positive) - xn i) + CReal_abs (xn i - inject_Q(proj1_sig (xn j) (4 * q)%positive)))).
+  unfold Qminus.
+  rewrite inject_Q_plus, opp_inject_Q.
+  setoid_replace (inject_Q (proj1_sig (xn i) (4 * p)%positive) +
+                  - inject_Q (proj1_sig (xn j) (4 * q)%positive))
+    with (inject_Q (proj1_sig (xn i) (4 * p)%positive) - xn i
+          + (xn i - inject_Q (proj1_sig (xn j) (4 * q)%positive))).
+  2: ring.
+  apply CReal_abs_triang. apply CReal_plus_le_lt_compat.
+  rewrite CReal_abs_minus_sym. apply (CReal_le_trans _ (inject_Q (1# 4*p))).
+  apply CReal_cv_self. apply inject_Q_le. unfold Qle, Qnum, Qden.
+  rewrite Z.mul_1_l, Z.mul_1_l.
+  apply Pos2Z.pos_le_pos. apply (Pos.le_trans _ (4*n)).
+  apply Pos.mul_le_mono_r. discriminate.
+  apply Pos.mul_le_mono_l. exact H0.
+  apply (CReal_le_lt_trans
+           _ (CReal_abs (xn i - xn j + (xn j - inject_Q (proj1_sig (xn j) (4 * q)%positive))))).
+  apply CReal_abs_morph. ring.
+  apply (CReal_le_lt_trans _ _ _ (CReal_abs_triang _ _)).
+  rewrite inject_Q_plus. apply CReal_plus_le_lt_compat.
+  apply (CReal_le_trans _ _ _ H). apply inject_Q_le.
+  unfold Qle, Qnum, Qden. rewrite Z.mul_1_l, Z.mul_1_l.
+  apply Pos2Z.pos_le_pos. apply Pos.mul_le_mono_r. discriminate.
+  apply (CReal_le_lt_trans _ (inject_Q (1#4*q))).
+  apply CReal_cv_self. apply inject_Q_lt. unfold Qlt, Qnum, Qden.
+  rewrite Z.mul_1_l, Z.mul_1_l.
+  apply Pos2Z.pos_lt_pos. apply (Pos.lt_le_trans _ (4*n)).
+  apply Pos.mul_lt_mono_r. reflexivity.
+  apply Pos.mul_le_mono_l. exact H1.
 Qed.
 
 Lemma Rcauchy_complete : forall (xn : nat -> CReal),
@@ -350,49 +216,63 @@ Lemma Rcauchy_complete : forall (xn : nat -> CReal),
     -> { l : CReal  &  seq_cv xn l }.
 Proof.
   intros xn cau.
-  destruct (R_has_all_rational_limits (fun n => let (l,_) := RQ_limit (xn n) n in l)
-                                      (Rdiag_cauchy_sequence xn cau))
-    as [l cv].
-  exists l. intro p. specialize (cv (2*p)%positive) as [k cv].
-  exists (max k (2 * Pos.to_nat p)). intros p0 H.
-  specialize (cv p0 (le_trans _ _ _ (Nat.le_max_l _ _) H)).
-  destruct (RQ_limit (xn p0) p0) as [q maj].
-  apply CReal_abs_le. split.
-  - apply (CReal_le_trans _ (inject_Q q - inject_Q (1 # 2 * p) - l)).
-    + unfold CReal_minus. rewrite (CReal_plus_comm (inject_Q q)).
-      apply (CReal_plus_le_reg_r (inject_Q (1 # p) + l - inject_Q q)).
-      ring_simplify. unfold CReal_minus.
-      rewrite <- (opp_inject_Q (1# 2*p)), <- inject_Q_plus.
-      setoid_replace ((1 # p) + - (1 # 2* p))%Q with (1#2*p)%Q.
-      rewrite CReal_abs_minus_sym in cv.
-      exact (CReal_le_trans _ _ _ (CReal_le_abs _) cv).
-      setoid_replace (1#p)%Q with (2 # 2*p)%Q.
-      rewrite Qinv_minus_distr. reflexivity. reflexivity.
-    + unfold CReal_minus.
-      do 2 rewrite <- (CReal_plus_comm (-l)). apply CReal_plus_le_compat_l.
-      apply (CReal_plus_le_reg_r (inject_Q (1 # 2 * p))).
-      ring_simplify. rewrite CReal_plus_comm.
-      apply (CReal_le_trans _ (xn p0 + inject_Q (1 # Pos.of_nat p0))).
-      apply CRealLt_asym, maj. apply CReal_plus_le_compat_l.
-      apply inject_Q_le.
-      apply Z2Nat.inj_le. discriminate. discriminate.
-      simpl. assert ((Pos.to_nat p~0 <= p0)%nat).
-      { apply (le_trans _ (Init.Nat.max k (2 * Pos.to_nat p))).
-        2: apply H. replace (p~0)%positive with (2*p)%positive.
-        2: reflexivity. rewrite Pos2Nat.inj_mul.
-        apply Nat.le_max_r. }
-      rewrite Nat2Pos.id. apply H0. intro abs. subst p0.
-      inversion H0. pose proof (Pos2Nat.is_pos (p~0)).
-      rewrite H2 in H1. inversion H1.
-  - apply (CReal_le_trans _ (inject_Q q - l)).
-    + unfold CReal_minus. do 2 rewrite <- (CReal_plus_comm (-l)).
-      apply CReal_plus_le_compat_l. apply CRealLt_asym, maj.
-    + apply (CReal_le_trans _ (inject_Q (1 # 2 * p))).
-      exact (CReal_le_trans _ _ _ (CReal_le_abs _) cv).
-      apply inject_Q_le. rewrite <- Qplus_0_r.
-      setoid_replace (1#p)%Q with ((1#2*p)+(1#2*p))%Q.
-      apply Qplus_le_r. discriminate.
-      rewrite Qinv_plus_distr. reflexivity.
+  exists (exist _ (fun n : positive =>
+                let (p, _) := cau (4 * n)%positive in
+                proj1_sig (xn p) (4 * n)%positive)
+           (Rcauchy_limit xn cau)).
+  intro p.
+  pose proof (CReal_cv_self (exist _ (fun n : positive =>
+                let (p, _) := cau (4 * n)%positive in
+                proj1_sig (xn p) (4 * n)%positive)
+           (Rcauchy_limit xn cau)) (2*p)) as H.
+  simpl (inject_Q
+           (proj1_sig
+              (exist (fun x : positive -> Q => QCauchySeq x id)
+                 (fun n : positive =>
+                  let (p, _) := cau (4 * n)%positive in
+                  proj1_sig (xn p) (4 * n)%positive) (Rcauchy_limit xn cau))
+              (2 * p)%positive)) in H.
+  pose proof (cau (2*p)%positive) as [k cv].
+  destruct (cau (p~0~0~0)%positive) as [i imaj].
+  (* The convergence modulus does not matter here, because a converging Cauchy
+     sequence always converges to its limit with twice the Cauchy modulus. *)
+  exists (max k i).
+  intros j H0.
+  setoid_replace (xn j -
+     exist (fun x : positive -> Q => QCauchySeq x id)
+       (fun n : positive =>
+        let (p0, _) := cau (4 * n)%positive in proj1_sig (xn p0) (4 * n)%positive)
+       (Rcauchy_limit xn cau))
+    with (xn j - inject_Q (proj1_sig (xn i) (p~0~0~0)%positive)
+          + (inject_Q (proj1_sig (xn i) (p~0~0~0)%positive) -
+     exist (fun x : positive -> Q => QCauchySeq x id)
+       (fun n : positive =>
+        let (p0, _) := cau (4 * n)%positive in proj1_sig (xn p0) (4 * n)%positive)
+       (Rcauchy_limit xn cau))).
+  2: ring. apply (CReal_le_trans _ _ _ (CReal_abs_triang _ _)).
+  apply (CReal_le_trans _ (inject_Q (1#2*p) + inject_Q (1#2*p))).
+  apply CReal_plus_le_compat.
+  2: rewrite CReal_abs_minus_sym; exact H.
+  specialize (imaj j i (le_trans _ _ _ (Nat.le_max_r _ _) H0) (le_refl _)).
+  apply (CReal_le_trans _ (inject_Q (1 # 4 * p) + inject_Q (1 # 4 * p))).
+  setoid_replace (xn j - inject_Q (proj1_sig (xn i) (p~0~0~0)%positive))
+    with (xn j - xn i
+          + (xn i - inject_Q (proj1_sig (xn i) (p~0~0~0)%positive))).
+  2: ring. apply (CReal_le_trans _ _ _ (CReal_abs_triang _ _)).
+  apply CReal_plus_le_compat. apply (CReal_le_trans _ _ _ imaj).
+  apply inject_Q_le. unfold Qle, Qnum, Qden.
+  rewrite Z.mul_1_l, Z.mul_1_l.
+  apply Pos2Z.pos_le_pos.
+  apply (Pos.mul_le_mono_r p 4 8). discriminate.
+  apply (CReal_le_trans _ _ _ (CReal_cv_self (xn i) (8*p))).
+  apply inject_Q_le. unfold Qle, Qnum, Qden.
+  rewrite Z.mul_1_l, Z.mul_1_l.
+  apply Pos2Z.pos_le_pos.
+  apply (Pos.mul_le_mono_r p 4 8). discriminate.
+  rewrite <- inject_Q_plus. rewrite (inject_Q_morph _ (1#2*p)).
+  apply CRealLe_refl. rewrite Qinv_plus_distr; reflexivity.
+  rewrite <- inject_Q_plus. rewrite (inject_Q_morph _ (1#p)).
+  apply CRealLe_refl. rewrite Qinv_plus_distr; reflexivity.
 Qed.
 
 Lemma CRealLtIsLinear : isLinearOrder CRealLt.
diff --git a/theories/Reals/ClassicalDedekindReals.v b/theories/Reals/ClassicalDedekindReals.v
index bb1ee93610..21f3a9cfca 100644
--- a/theories/Reals/ClassicalDedekindReals.v
+++ b/theories/Reals/ClassicalDedekindReals.v
@@ -149,32 +149,31 @@ 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))).
+   {(fun n0 : nat => (proj1_sig x (Pos.of_nat (S n0)) <= q + (1 # Pos.of_nat (S n0)))%Q) n} +
+   {~ (fun n0 : nat => (proj1_sig x (Pos.of_nat (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 (Pos.of_nat (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)
+  exists (fun q:Q => if sig_forall_dec (fun n:nat => Qle (proj1_sig x (Pos.of_nat (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)
+    destruct (sig_forall_dec (fun n : nat => (proj1_sig x (Pos.of_nat (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)
+    destruct (sig_forall_dec (fun n : nat => (proj1_sig x (Pos.of_nat (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)
+    destruct (sig_forall_dec (fun n : nat => (proj1_sig x (Pos.of_nat (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).
@@ -187,7 +186,7 @@ Proof.
     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)
+    destruct (sig_forall_dec (fun n : nat => (proj1_sig x (Pos.of_nat (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.
@@ -195,30 +194,30 @@ Proof.
     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)).
+    apply (Qplus_lt_l _ _ (xn 1%positive - 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)).
+    destruct (sig_forall_dec (fun n : nat => (proj1_sig x (Pos.of_nat (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).
+    specialize (abs ((q + xn (Pos.of_nat (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)).
+            (xn (Pos.of_nat (S n0)) <= (q + xn (Pos.of_nat (S n)) - (1 # Pos.of_nat (S n))) / 2 + (1 # Pos.of_nat (S n0)))%Q)
+           (H ((q + xn (Pos.of_nat (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.
+      apply (Qplus_le_l _ _ (-xn (Pos.of_nat (S n)))) in q0. ring_simplify in q0.
       contradiction. reflexivity.
 Defined.
 
@@ -234,23 +233,24 @@ Qed.
 
 Definition DRealRepr : DReal -> CReal.
 Proof.
-  intro x. exists (fun n => proj1_sig (DRealQlim x n)).
+  intro x. exists (fun n:positive => proj1_sig (DRealQlim x (Pos.to_nat n))).
   intros n p q H H0.
-  destruct (DRealQlim x p), (DRealQlim x q); unfold proj1_sig.
+  destruct (DRealQlim x (Pos.to_nat p)), (DRealQlim x (Pos.to_nat 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))).
+  - intros. apply (Qlt_le_trans _ (1 # Pos.of_nat (S (Pos.to_nat 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 Pos2Nat.inj_le. rewrite Nat2Pos.id.
+    apply le_S, Pos2Nat.inj_le, H0. discriminate.
+  - intros. apply (Qlt_le_trans _ (1 # Pos.of_nat (S (Pos.to_nat 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.
+    apply Pos2Nat.inj_le. rewrite Nat2Pos.id.
+    apply le_S, Pos2Nat.inj_le, H. discriminate.
 Defined.
 
 Definition Rle (x y : DReal)
@@ -390,15 +390,15 @@ 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.
+    -> (proj1_sig x (Pos.of_nat (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)
+        sig_forall_dec (fun n : nat => (xn (Pos.of_nat (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)
+           match Qlt_le_dec (q + (1 # Pos.of_nat (S n))) (xn (Pos.of_nat (S n))) with
+           | left q0 => right (Qlt_not_le (q + (1 # Pos.of_nat (S n))) (xn (Pos.of_nat (S n))) q0)
            | right q0 => left q0
            end)).
   discriminate. apply q0.
@@ -417,9 +417,10 @@ Proof.
     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).
+    ring_simplify. rewrite Pos2Nat.id in qmaj.
+    apply (Qle_trans _ _ _ qmaj).
     rewrite <- Qplus_assoc. apply Qplus_le_r.
-    rewrite Pos2Nat.id. apply (Qle_trans _ ((1#p)+(1#p))).
+    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.
@@ -434,30 +435,32 @@ Proof.
     (* 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)
+           sig_forall_dec (fun n : nat => (xn (Pos.of_nat (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
+              match Qlt_le_dec (q + (1 # Pos.of_nat (S n))) (xn (Pos.of_nat (S n))) with
               | left q0 =>
-                  right (Qlt_not_le (q + (1 # Pos.of_nat (S n))) (xn (S n)) q0)
+                  right (Qlt_not_le (q + (1 # Pos.of_nat (S n))) (xn (Pos.of_nat (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.
+    apply (Qplus_lt_l _ _ (xn 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)))).
+    apply (Qlt_trans _ ((2 # p) + xn p + (1 # Pos.of_nat (S n)))).
     2: exact pmaj.
-    apply (Qplus_lt_l _ _ (-xn (Pos.to_nat p))).
+    apply (Qplus_lt_l _ _ (-xn 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)).
+    + specialize (xcau (Pos.of_nat (S n)) (Pos.of_nat (S n)) p).
       apply (Qlt_trans _ (1# Pos.of_nat (S n))). apply xcau.
-      rewrite Nat2Pos.id. apply le_refl. discriminate.
+      apply Pos.le_refl. unfold id. apply Pos2Nat.inj_le.
       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.
+      apply le_S_n in l. unfold id. apply Pos2Nat.inj_le.
+      rewrite Nat2Pos.id.
+      apply le_S, l. discriminate. apply Pos.le_refl.
       ring_simplify. apply (Qlt_trans _ (2#p)).
       unfold Qlt, Qnum, Qden.
       apply Z.mul_lt_mono_pos_r. reflexivity. reflexivity.