From 9dc1f1fd48484b00d67871b6869a4c0c48e26f26 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 22 Oct 2018 22:38:21 +0200
Subject: Elementary properties about IZR for generic use.

---
 theories/Reals/RIneq.v | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)

diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index 33e40a115b..4fa8b3216a 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -1774,6 +1774,28 @@ Proof.
   now rewrite <- INR_IPR, SuccNat2Pos.id_succ.
 Qed.
 
+Lemma IZR_NEG : forall p, IZR (Zneg p) = Ropp (IZR (Zpos p)).
+Proof.
+  reflexivity.
+Qed.
+
+(** The three following lemmas map the default form of numerical
+    constants to their representation in terms of the axioms of
+    [R]. This can be a useful intermediate representation for reifying
+    to another axiomatics of the reals. It is however generally more
+    convenient to keep constants represented under an [IZR z] form when
+    working within [R]. *)
+
+Lemma IZR_POS_xO : forall p, IZR (Zpos (xO p)) = (1+1) * (IZR (Zpos p)).
+Proof.
+  intro. unfold IZR, IPR. destruct p; simpl; trivial. rewrite Rmult_1_r. trivial.
+Qed.
+
+Lemma IZR_POS_xI : forall p, IZR (Zpos (xI p)) = 1 + (1+1) * IZR (Zpos p).
+Proof.
+  intro. unfold IZR, IPR. destruct p; simpl; trivial. rewrite Rmult_1_r. trivial.
+Qed.
+
 Lemma plus_IZR_NEG_POS :
   forall p q:positive, IZR (Zpos p + Zneg q) = IZR (Zpos p) + IZR (Zneg q).
 Proof.
-- 
cgit v1.2.3