From ea9397e3da37f35d088488be141cb18cc38ea11b Mon Sep 17 00:00:00 2001
From: jadep <jade.philipoom@gmail.com>
Date: Mon, 25 Jul 2016 21:04:23 -0400
Subject: A couple new util lemmas

---
 src/Util/ZUtil.v | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

(limited to 'src/Util/ZUtil.v')

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.
-- 
cgit v1.2.3