diff options
Diffstat (limited to 'src/Util/ZUtil/Land.v')
| -rw-r--r-- | src/Util/ZUtil/Land.v | 15 |
1 files changed, 14 insertions, 1 deletions
diff --git a/src/Util/ZUtil/Land.v b/src/Util/ZUtil/Land.v index f46d541e9..7f27f942d 100644 --- a/src/Util/ZUtil/Land.v +++ b/src/Util/ZUtil/Land.v @@ -1,6 +1,8 @@ Require Import Coq.ZArith.ZArith. +Require Import Coq.micromega.Lia. Require Import Crypto.Util.ZUtil.Notations. -Local Open Scope Z_scope. +Require Import Crypto.Util.ZUtil.Definitions. +Local Open Scope bool_scope. Local Open Scope Z_scope. Module Z. Lemma land_same_r : forall a b, (a &' b) &' b = a &' b. @@ -10,4 +12,15 @@ Module Z. case_eq (Z.testbit b n); intros; rewrite ?Bool.andb_true_r, ?Bool.andb_false_r; reflexivity. Qed. + + Lemma land_m1'_l a : Z.land (-1) a = a. + Proof. apply Z.land_m1_l. Qed. + Hint Rewrite Z.land_m1_l land_m1'_l : zsimplify_const zsimplify zsimplify_fast. + + Lemma land_m1'_r a : Z.land a (-1) = a. + Proof. apply Z.land_m1_r. Qed. + Hint Rewrite Z.land_m1_r land_m1'_r : zsimplify_const zsimplify zsimplify_fast. + + Lemma sub_1_lt_le x y : (x - 1 < y) <-> (x <= y). + Proof. lia. Qed. End Z. |