Merge pull request #66 from affeldt-aist/fixes_65

fixes issue #65
affeldt-aist · Sep 29, 2021 · 7f724db · 7f724db
2 parents d87b329 + b127907
commit 7f724db
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 0 deletions.
diff --git 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
@@ -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.