diff options
Diffstat (limited to 'src/Arithmetic/MontgomeryReduction/Proofs.v')
| -rw-r--r-- | src/Arithmetic/MontgomeryReduction/Proofs.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/Arithmetic/MontgomeryReduction/Proofs.v b/src/Arithmetic/MontgomeryReduction/Proofs.v index 5f459e52d..e6be440fb 100644 --- a/src/Arithmetic/MontgomeryReduction/Proofs.v +++ b/src/Arithmetic/MontgomeryReduction/Proofs.v @@ -4,7 +4,9 @@ Wikipedia. *) Require Import Coq.ZArith.ZArith Coq.micromega.Psatz Coq.Structures.Equalities. Require Import Crypto.Arithmetic.MontgomeryReduction.Definition. -Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.ZUtil.EquivModulo. +Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo. +Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.Tactics.SimplifyRepeatedIfs. Require Import Crypto.Util.Notations. |