diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-07-25 21:04:23 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-07-25 21:04:23 -0400 |
| commit | ea9397e3da37f35d088488be141cb18cc38ea11b (patch) | |
| tree | 2cb1f857951e2388b79253cb5be123f2b0d383fb /src/Util/ZUtil.v | |
| parent | e880359898151f81383844b602df0c6df7f88ad1 (diff) | |
A couple new util lemmas
Diffstat (limited to 'src/Util/ZUtil.v')
| -rw-r--r-- | src/Util/ZUtil.v | 7 |
1 files changed, 6 insertions, 1 deletions
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. |