diff options
Diffstat (limited to 'src/Util/ZUtil.v')
| -rw-r--r-- | src/Util/ZUtil.v | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 536566312..a5716fca4 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -2,6 +2,7 @@ Require Import Coq.ZArith.Zpower Coq.ZArith.Znumtheory Coq.ZArith.ZArith Coq.ZAr Require Import Coq.omega.Omega Coq.Numbers.Natural.Peano.NPeano Coq.Arith.Arith. Require Import Crypto.Util.NatUtil. Require Import Coq.Lists.List. +Import Nat. Local Open Scope Z. Lemma gt_lt_symmetry: forall n m, n > m <-> m < n. @@ -208,7 +209,7 @@ Proof. rewrite (le_plus_minus n m) at 1 by assumption. rewrite Nat2Z.inj_add. rewrite Z.pow_add_r by apply Nat2Z.is_nonneg. - rewrite <- Z.div_div by first + rewrite <- Z.div_div by first [ pose proof (Z.pow_pos_nonneg 2 (Z.of_nat n)); omega | apply Z.pow_pos_nonneg; omega ]. rewrite Z.div_add by (pose proof (Z.pow_pos_nonneg 2 (Z.of_nat n)); omega). @@ -332,7 +333,7 @@ Qed. replace (2 ^ (Z.pos p)) with (2 ^ (Z.pos p - 1)* 2). rewrite Z.div_add_l by omega. reflexivity. - replace 2 with (2 ^ 1) at 2 by auto. + change 2 with (2 ^ 1) at 2. rewrite <-Z.pow_add_r by (pose proof (Pos2Z.is_pos p); omega). f_equal. omega. Qed. @@ -345,7 +346,7 @@ Qed. + unfold Z.ones. rewrite Z.shiftr_0_r, Z.shiftl_1_l, Z.sub_0_r. omega. - + intros. + + intros. destruct (Z_lt_le_dec x n); try omega. intuition. left. @@ -360,7 +361,7 @@ Qed. Z.shiftr a i <= Z.ones (n - i) . Proof. intros a n i G G0 G1. - destruct (Z_le_lt_eq_dec i n G1). + destruct (Z_le_lt_eq_dec i n G1). + destruct (Z_shiftr_ones' a n G i G0); omega. + subst; rewrite Z.sub_diag. destruct (Z_eq_dec a 0). |