diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-05-13 12:14:27 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-05-13 12:14:27 -0400 |
| commit | a30bbfe60d619e13601985340b1b70b150aecc28 (patch) | |
| tree | 778062d35ecd7beb8f5c3a8e6fcc2292e1ade3af /src/Util/ZUtil/Land.v | |
| parent | 6e5dfa6ad6aca6aa19b7d1348817bd2c23d8fdad (diff) | |
Split off more of ZUtil
Diffstat (limited to 'src/Util/ZUtil/Land.v')
| -rw-r--r-- | src/Util/ZUtil/Land.v | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/src/Util/ZUtil/Land.v b/src/Util/ZUtil/Land.v new file mode 100644 index 000000000..b3d3f3727 --- /dev/null +++ b/src/Util/ZUtil/Land.v @@ -0,0 +1,13 @@ +Require Import Coq.ZArith.ZArith. +Require Import Crypto.Util.ZUtil.Notations. +Local Open Scope Z_scope. + +Module Z. + Lemma land_same_r : forall a b, (a &' b) &' b = a &' b. + Proof. + intros; apply Z.bits_inj'; intros. + rewrite !Z.land_spec. + case_eq (Z.testbit b n); intros; + rewrite ?Bool.andb_true_r, ?Bool.andb_false_r; reflexivity. + Qed. +End Z. |