diff options
Diffstat (limited to 'src/ModularArithmetic/ModularBaseSystemList.v')
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystemList.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/ModularArithmetic/ModularBaseSystemList.v b/src/ModularArithmetic/ModularBaseSystemList.v index cbab03d6a..b46429fcc 100644 --- a/src/ModularArithmetic/ModularBaseSystemList.v +++ b/src/ModularArithmetic/ModularBaseSystemList.v @@ -1,4 +1,5 @@ Require Import Coq.ZArith.Zpower Coq.ZArith.ZArith. +Require Import Coq.Numbers.Natural.Peano.NPeano. Require Import Coq.Lists.List. Require Import Crypto.Util.ListUtil Crypto.Util.CaseUtil Crypto.Util.ZUtil. Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. |