diff options
Diffstat (limited to 'src/ModularArithmetic/Pre.v')
| -rw-r--r-- | src/ModularArithmetic/Pre.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/ModularArithmetic/Pre.v b/src/ModularArithmetic/Pre.v index 5e61278f6..8566d30ab 100644 --- a/src/ModularArithmetic/Pre.v +++ b/src/ModularArithmetic/Pre.v @@ -5,6 +5,7 @@ Require Import Crypto.Tactics.VerdiTactics. Require Import Coq.omega.Omega. Require Import Crypto.Util.NumTheoryUtil. Require Import Crypto.Tactics.VerdiTactics. +Require Export Crypto.Util.FixCoqMistakes. Lemma Z_mod_mod x m : x mod m = (x mod m) mod m. symmetry. |