A couple new util lemmas

2 files changed, 11 insertions, 1 deletions

diff --git a/src/Util/NatUtil.v b/src/Util/NatUtil.v
index 1c144281b..84fbb11eb 100644
--- a/src/Util/NatUtil.v
+++ b/src/Util/NatUtil.v
@@ -64,6 +64,11 @@ Proof.
   reflexivity.
 Qed.
 
+Lemma pred_mod : forall m, (0 < m)%nat -> ((pred m) mod m)%nat = Init.Nat.pred m.
+Proof.
+  intros; apply Nat.mod_small; omega.
+Qed.
+
 Lemma div_add_l' : forall a b c, a <> 0 -> (a * b + c) / a = b + c / a.
 Proof.
   intros; rewrite Nat.mul_comm; auto using div_add_l.
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index 50962cb4d..5811aa1a8 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -335,7 +335,6 @@ Module Z.
     reflexivity.
   Qed.
 
-
   Definition shiftl_by n a := Z.shiftl a n.
 
   Lemma shiftl_by_mul_pow2 : forall n a, 0 <= n -> Z.mul (2 ^ n) a = Z.shiftl_by n a.
@@ -400,6 +399,12 @@ Module Z.
     apply Z.div_le_mono; omega.
   Qed.
 
+  Lemma shiftr_le : forall a b i : Z, 0 <= i -> a <= b -> a >> i <= b >> i.
+  Proof.
+    intros until 1. revert a b. apply natlike_ind with (x := i); intros; auto.
+    rewrite !shiftr_succ, shiftr_1_r_le; eauto. reflexivity.
+  Qed.
+
   Lemma ones_pred : forall i, 0 < i -> Z.ones (Z.pred i) = Z.shiftr (Z.ones i) 1.
   Proof.
     induction i; [ | | pose proof (Pos2Z.neg_is_neg p) ]; try omega.