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
```

7 files changed, 14 insertions, 14 deletions

diff --git a/src/Util/CaseUtil.v b/src/Util/CaseUtil.v
index 35f207ffc..af04a1e49 100644
--- a/src/Util/CaseUtil.v
+++ b/src/Util/CaseUtil.v
@@ -1,4 +1,4 @@
-Require Import Arith.
+Require Import Coq.Arith.Arith.
 
 Ltac case_max :=
   match goal with [ |- context[max ?x ?y] ] =>
diff --git a/src/Util/IterAssocOp.v b/src/Util/IterAssocOp.v
index 4524f5cb9..016a4f7bd 100644
--- a/src/Util/IterAssocOp.v
+++ b/src/Util/IterAssocOp.v
@@ -1,5 +1,5 @@
 Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms Coq.Classes.Equivalence.
-Require Import NArith BinPosDef.
+Require Import Coq.NArith.NArith Coq.PArith.BinPosDef.
 Local Open Scope equiv_scope.
 
 Generalizable All Variables.
diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v
index 783e3f527..1f9a62457 100644
--- a/src/Util/ListUtil.v
+++ b/src/Util/ListUtil.v
@@ -1,7 +1,7 @@
-Require Import List.
-Require Import Omega.
-Require Import Arith.Peano_dec.
-Require Import VerdiTactics.
+Require Import Coq.Lists.List.
+Require Import Coq.omega.Omega.
+Require Import Coq.Arith.Peano_dec.
+Require Import Crypto.Tactics.VerdiTactics.
 
 Ltac boring :=
   simpl; intuition;
diff --git a/src/Util/NatUtil.v b/src/Util/NatUtil.v
index 4ba6d0808..6a62d6c22 100644
--- a/src/Util/NatUtil.v
+++ b/src/Util/NatUtil.v
@@ -1,4 +1,4 @@
-Require Import NPeano Omega.
+Require Import Coq.Numbers.Natural.Peano.NPeano Coq.omega.Omega.
 
 Local Open Scope nat_scope.
 
diff --git a/src/Util/NumTheoryUtil.v b/src/Util/NumTheoryUtil.v
index 5acef8b75..10ce148b0 100644
--- a/src/Util/NumTheoryUtil.v
+++ b/src/Util/NumTheoryUtil.v
@@ -1,8 +1,8 @@
-Require Import Zpower Znumtheory ZArith.ZArith ZArith.Zdiv.
-Require Import Omega NPeano Arith.
+Require Import Coq.ZArith.Zpower Coq.ZArith.Znumtheory Coq.ZArith.ZArith Coq.ZArith.Zdiv.
+Require Import Coq.omega.Omega Coq.Numbers.Natural.Peano.NPeano Coq.Arith.Arith.
 Require Import Crypto.Util.NatUtil Crypto.Util.ZUtil.
 Require Import Coqprime.Zp.
-Require Import VerdiTactics.
+Require Import Crypto.Tactics.VerdiTactics.
 Local Open Scope Z.
 
 (* TODO: move somewhere else for lemmas about Coqprime? *)
diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v
index 49de971ef..17d04c60a 100644
--- a/src/Util/WordUtil.v
+++ b/src/Util/WordUtil.v
@@ -1,5 +1,5 @@
-Require Import NPeano.
-Require Import ZArith.ZArith.
+Require Import Coq.Numbers.Natural.Peano.NPeano.
+Require Import Coq.ZArith.ZArith.
 Require Import Bedrock.Word.
 
 Local Open Scope nat_scope.
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index 2cfab2e90..db3d84b2d 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -1,5 +1,5 @@
-Require Import Zpower Znumtheory ZArith.ZArith ZArith.Zdiv.
-Require Import Omega NPeano Arith.
+Require Import Coq.ZArith.Zpower Coq.ZArith.Znumtheory Coq.ZArith.ZArith Coq.ZArith.Zdiv.
+Require Import Coq.omega.Omega Coq.Numbers.Natural.Peano.NPeano Coq.Arith.Arith.
 Require Import Crypto.Util.NatUtil.
 Local Open Scope Z.