blob: b3d3f372774c829580acd861c86daab77dfe57a1 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
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.
|
