blob: 7f27f942d90c8f3f02cd1f6768059c14614ca5bc (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
|
Require Import Coq.ZArith.ZArith.
Require Import Coq.micromega.Lia.
Require Import Crypto.Util.ZUtil.Notations.
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.
Proof.
intros a b; apply Z.bits_inj'; intros n H.
rewrite !Z.land_spec.
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.
|
