diff options
Diffstat (limited to 'src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v')
| -rw-r--r-- | src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v b/src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v index 45566839a..b23e0ff1b 100644 --- a/src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v +++ b/src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v @@ -8,9 +8,13 @@ Require Import Crypto.Compilers.Z.Bounds.Interpretation. Require Import Crypto.Compilers.Z.Bounds.InterpretationLemmas.Tactics. Require Import Crypto.Compilers.SmartMap. Require Import Crypto.Util.ZRange.CornersMonotoneBounds. -Require Import Crypto.Util.ZUtil. Require Import Crypto.Util.ZUtil.Stabilization. Require Import Crypto.Util.ZUtil.MulSplit. +Require Import Crypto.Util.ZUtil.Modulo. +Require Import Crypto.Util.ZUtil.LandLorShiftBounds. +Require Import Crypto.Util.ZUtil.Morphisms. +Require Import Crypto.Util.ZUtil.Definitions. +Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. Require Import Crypto.Util.PointedProp. Require Import Crypto.Util.Bool. Require Import Crypto.Util.FixedWordSizesEquality. |