diff options
Diffstat (limited to 'theories/Numbers/Cyclic/Int63')
| -rw-r--r-- | theories/Numbers/Cyclic/Int63/Int63.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/theories/Numbers/Cyclic/Int63/Int63.v b/theories/Numbers/Cyclic/Int63/Int63.v index 383c0aff3a..dbca2f0947 100644 --- a/theories/Numbers/Cyclic/Int63/Int63.v +++ b/theories/Numbers/Cyclic/Int63/Int63.v @@ -290,6 +290,7 @@ Proof. intros h; apply Z.lt_gt, Zpower_gt_0; lia. Qed. Lemma pow2_nz n : 0 <= n → 2 ^ n ≠ 0. Proof. intros h; generalize (pow2_pos _ h); lia. Qed. +#[global] Hint Resolve pow2_pos pow2_nz : zarith. (* =================================================== *) |