diff options
Diffstat (limited to 'src/Arithmetic/Saturated/UniformWeight.v')
| -rw-r--r-- | src/Arithmetic/Saturated/UniformWeight.v | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/Arithmetic/Saturated/UniformWeight.v b/src/Arithmetic/Saturated/UniformWeight.v index bd351b6cd..bf069f2d6 100644 --- a/src/Arithmetic/Saturated/UniformWeight.v +++ b/src/Arithmetic/Saturated/UniformWeight.v @@ -4,7 +4,9 @@ Local Open Scope Z_scope. Require Import Crypto.Arithmetic.Core. Require Import Crypto.Arithmetic.Saturated.Core. -Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.ZUtil.Le. +Require Import Crypto.Util.ZUtil.Modulo. +Require Import Crypto.Util.ZUtil.Tactics.PeelLe. Require Import Crypto.Util.LetIn Crypto.Util.Tuple. Local Notation "A ^ n" := (tuple A n) : type_scope. @@ -88,4 +90,4 @@ Section UniformWeight. Definition small {n} (p : Z^n) : Prop := forall x, In x (to_list _ p) -> 0 <= x < bound. -End UniformWeight.
\ No newline at end of file +End UniformWeight. |