Finish absolutizing imports

The file coqprime/Coqprime/ListAux.v was importing List, which was confusing
machines on which mathclasses was also installed.

Using https://github.com/JasonGross/coq-tools
```bash
make -kj10
cd src
git ls-files "*.v" | xargs python ~/Documents/repos/coq-tools/absolutize-imports.py -i -R . Crypto
```

6 files changed, 15 insertions, 15 deletions

diff --git a/src/Spec/CompleteEdwardsCurve.v b/src/Spec/CompleteEdwardsCurve.v
index 23e201405..8dbfdf7b9 100644
--- a/src/Spec/CompleteEdwardsCurve.v
+++ b/src/Spec/CompleteEdwardsCurve.v
@@ -1,4 +1,4 @@
-Require BinInt Znumtheory.
+Require Coq.ZArith.BinInt Coq.ZArith.Znumtheory.
 
 Require Crypto.CompleteEdwardsCurve.Pre.
 
diff --git a/src/Spec/Ed25519.v b/src/Spec/Ed25519.v
index e16cc73f6..92c36b56c 100644
--- a/src/Spec/Ed25519.v
+++ b/src/Spec/Ed25519.v
@@ -1,14 +1,14 @@
-Require Import ZArith.ZArith Zpower ZArith Znumtheory.
-Require Import NPeano NArith.
+Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory.
+Require Import Coq.Numbers.Natural.Peano.NPeano Coq.NArith.NArith.
 Require Import Crypto.Spec.Encoding Crypto.Spec.PointEncoding.
 Require Import Crypto.Spec.EdDSA.
 Require Import Crypto.Spec.CompleteEdwardsCurve Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems.
 Require Import Crypto.ModularArithmetic.PrimeFieldTheorems Crypto.ModularArithmetic.ModularArithmeticTheorems.
 Require Import Crypto.Util.NatUtil Crypto.Util.ZUtil Crypto.Util.WordUtil Crypto.Util.NumTheoryUtil.
 Require Import Bedrock.Word.
-Require Import VerdiTactics.
-Require Import Decidable.
-Require Import Omega.
+Require Import Crypto.Tactics.VerdiTactics.
+Require Import Coq.Logic.Decidable.
+Require Import Coq.omega.Omega.
 
 Local Open Scope nat_scope.
 Definition q : Z := (2 ^ 255 - 19)%Z.
diff --git a/src/Spec/EdDSA.v b/src/Spec/EdDSA.v
index 45950f6a1..6f57d7bec 100644
--- a/src/Spec/EdDSA.v
+++ b/src/Spec/EdDSA.v
@@ -4,8 +4,8 @@ Require Import Crypto.Spec.CompleteEdwardsCurve.
 
 Require Import Crypto.Util.WordUtil.
 Require Bedrock.Word.
-Require Znumtheory BinInt.
-Require NPeano.
+Require Coq.ZArith.Znumtheory Coq.ZArith.BinInt.
+Require Coq.Numbers.Natural.Peano.NPeano.
 
 Coercion Word.wordToNat : Word.word >-> nat.
 
diff --git a/src/Spec/Encoding.v b/src/Spec/Encoding.v
index 7bef9295b..14cf9d9d9 100644
--- a/src/Spec/Encoding.v
+++ b/src/Spec/Encoding.v
@@ -1,8 +1,8 @@
-Require Import ZArith.ZArith Zpower ZArith.
-Require Import NPeano.
+Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith.
+Require Import Coq.Numbers.Natural.Peano.NPeano.
 Require Import Crypto.ModularArithmetic.PrimeFieldTheorems Crypto.ModularArithmetic.ModularArithmeticTheorems.
 Require Import Bedrock.Word.
-Require Import VerdiTactics.
+Require Import Crypto.Tactics.VerdiTactics.
 Require Import Crypto.Util.NatUtil.
 Require Import Crypto.Util.WordUtil.
 
diff --git a/src/Spec/ModularArithmetic.v b/src/Spec/ModularArithmetic.v
index da6a62ada..76efe3d79 100644
--- a/src/Spec/ModularArithmetic.v
+++ b/src/Spec/ModularArithmetic.v
@@ -1,4 +1,4 @@
-Require Znumtheory BinNums.
+Require Coq.ZArith.Znumtheory Coq.Numbers.BinNums.
 
 Require Crypto.ModularArithmetic.Pre.
 
diff --git a/src/Spec/PointEncoding.v b/src/Spec/PointEncoding.v
index 2fec05863..4823ef28f 100644
--- a/src/Spec/PointEncoding.v
+++ b/src/Spec/PointEncoding.v
@@ -1,11 +1,11 @@
-Require Import ZArith.ZArith Zpower ZArith Znumtheory.
-Require Import NPeano NArith.
+Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory.
+Require Import Coq.Numbers.Natural.Peano.NPeano Coq.NArith.NArith.
 Require Import Crypto.Spec.Encoding Crypto.Encoding.EncodingTheorems.
 Require Import Crypto.Spec.CompleteEdwardsCurve Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems.
 Require Import Crypto.ModularArithmetic.PrimeFieldTheorems Crypto.ModularArithmetic.ModularArithmeticTheorems.
 Require Import Crypto.Util.NatUtil Crypto.Util.ZUtil Crypto.Util.NumTheoryUtil.
 Require Import Bedrock.Word.
-Require Import VerdiTactics.
+Require Import Crypto.Tactics.VerdiTactics.
 
 Local Open Scope F_scope.