Add some ZUtil lemmas

2 files changed, 20 insertions, 0 deletions

diff --git a/src/Util/ZUtil/Ge.v b/src/Util/ZUtil/Ge.v
new file mode 100644
index 000000000..4b92881c4
--- /dev/null
+++ b/src/Util/ZUtil/Ge.v
@@ -0,0 +1,13 @@
+Require Import Coq.ZArith.ZArith Coq.Classes.RelationClasses.
+
+Local Open Scope Z_scope.
+
+Module Z.
+  Lemma ge_refl x : x >= x.
+  Proof. rewrite !Z.ge_le_iff; reflexivity. Qed.
+  Lemma ge_trans n m p : n >= m -> m >= p -> n >= p.
+  Proof. rewrite !Z.ge_le_iff; eauto using Z.le_trans. Qed.
+
+  Global Instance ge_preorder : PreOrder Z.ge.
+  Proof. constructor; hnf; [ apply ge_refl | apply ge_trans ]. Defined.
+End Z.
diff --git a/src/Util/ZUtil/Morphisms.v b/src/Util/ZUtil/Morphisms.v
index 285fa5261..d58b89c91 100644
--- a/src/Util/ZUtil/Morphisms.v
+++ b/src/Util/ZUtil/Morphisms.v
@@ -1,5 +1,6 @@
 (** * [Proper] morphisms for ℤ constants *)
 Require Import Coq.omega.Omega.
+Require Import Coq.micromega.Lia.
 Require Import Coq.ZArith.ZArith.
 Require Import Coq.Classes.Morphisms.
 Require Import Coq.Classes.RelationPairs.
@@ -11,14 +12,20 @@ Module Z.
       instances; making them instances would slow typeclass search
       unacceptably.  In files where we use these, we add them with
       [Local Existing Instances]. *)
+  Lemma succ_le_Proper : Proper (Z.le ==> Z.le) Z.succ.
+  Proof. repeat (omega || intro). Qed.
   Lemma add_le_Proper : Proper (Z.le ==> Z.le ==> Z.le) Z.add.
   Proof. repeat (omega || intro). Qed.
+  Lemma add_le_Proper' x : Proper (Z.le ==> Z.le) (Z.add x).
+  Proof. repeat (omega || intro). Qed.
   Lemma sub_le_ge_Proper : Proper (Z.le ==> Z.ge ==> Z.le) Z.sub.
   Proof. repeat (omega || intro). Qed.
   Lemma sub_le_flip_le_Proper : Proper (Z.le ==> Basics.flip Z.le ==> Z.le) Z.sub.
   Proof. unfold Basics.flip; repeat (omega || intro). Qed.
   Lemma sub_le_eq_Proper : Proper (Z.le ==> Logic.eq ==> Z.le) Z.sub.
   Proof. repeat (omega || intro). Qed.
+  Lemma mul_Zpos_le_Proper p : Proper (Z.le ==> Z.le) (Z.mul (Z.pos p)).
+  Proof. repeat (nia || intro). Qed.
   Lemma log2_up_le_Proper : Proper (Z.le ==> Z.le) Z.log2_up.
   Proof. intros ???; apply Z.log2_up_le_mono; assumption. Qed.
   Lemma log2_le_Proper : Proper (Z.le ==> Z.le) Z.log2.