From b1279072d2bf13db1e702a00faa7dafcb801378b Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Wed, 8 Sep 2021 16:42:55 +0900
Subject: [PATCH] fixes issue #65

---
 changelog.txt | 1 +
 lib/ssrZ.v    | 5 +++++
 2 files changed, 6 insertions(+)

diff --git a/changelog.txt b/changelog.txt
index 9556770b..ba8930dc 100644
--- a/changelog.txt
+++ b/changelog.txt
@@ -5,6 +5,7 @@ from 0.3.3 to 0.3.4
 * added:
 - in ssrZ.v:
   + lemmas ltZ_addl, ltZ_addr, pmulZ_rgt0
+  + lemmas intRD, leZ0n
 - in ssrR.v:
   + lemma expRn_gt0
 * renamed:
diff --git a/lib/ssrZ.v b/lib/ssrZ.v
index 96d5a48a..30bb34f0 100644
--- a/lib/ssrZ.v
+++ b/lib/ssrZ.v
@@ -39,6 +39,9 @@ Lemma natZ0 : 0%:Z = 0%Z. Proof. exact: Nat2Z.inj_0. Qed.
 
 Lemma natZS n : n.+1%:Z = n%:Z.+1Z. Proof. by rewrite -Zpos_P_of_succ_nat. Qed.
 
+(* TODO: is it the right name? *)
+Lemma intRD n m : (n + m)%:Z = (n%:Z + m%:Z)%Z. Proof. exact/Nat2Z.inj_add. Qed.
+
 Definition addZ0 := Zplus_0_r.
 Definition add0Z := Zplus_0_l.
 
@@ -351,6 +354,8 @@ Proof. by apply/idP/idP => /ltZP/ltZ_subRL/ltZP. Qed.
 
 Definition ltZ_addr_subl := ltZ_subRL.
 
+Lemma leZ0n n : 0 <= n%:Z. Proof. exact: Zle_0_nat. Qed.
+
 Lemma Z_S n : Z_of_nat n.+1 = Z_of_nat n + 1.
 Proof. by rewrite inj_S. Qed.