1 files changed, 19 insertions, 3 deletions
diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v
index 9fbda92a2..e9098104c 100644
--- a/theories/Reals/Raxioms.v
+++ b/theories/Reals/Raxioms.v
@@ -118,14 +118,30 @@ Arguments INR n%nat.
 (** *    Injection from [Z] to [R]                        *)
 (**********************************************************)
 
+(* compact representation for 2*p *)
+Fixpoint IPR_2 (p:positive) : R :=
+  match p with
+  | xH => 1 + 1
+  | xO p => (1 + 1) * IPR_2 p
+  | xI p => (1 + 1) * (1 + IPR_2 p)
+  end.
+
+Definition IPR (p:positive) : R :=
+  match p with
+  | xH => 1
+  | xO p => IPR_2 p
+  | xI p => 1 + IPR_2 p
+  end.
+Arguments IPR p%positive : simpl never.
+
 (**********)
 Definition IZR (z:Z) : R :=
   match z with
   | Z0 => 0
-  | Zpos n => INR (Pos.to_nat n)
-  | Zneg n => - INR (Pos.to_nat n)
+  | Zpos n => IPR n
+  | Zneg n => - IPR n
   end.
-Arguments IZR z%Z.
+Arguments IZR z%Z : simpl never.
 
 (**********************************************************)
 (** *    [R] Archimedean                                  *)