diff --git a/src/Algebra/Hierarchy.v b/src/Algebra/Hierarchy.v
index 426e81f8de..9c9e93eeab 100644
--- a/src/Algebra/Hierarchy.v
+++ b/src/Algebra/Hierarchy.v
@@ -5,7 +5,6 @@ Require Export Crypto.Util.Decidable.
 Require Coq.PArith.BinPos.
 Require Import Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop.
 
-Require Coq.Numbers.Natural.Peano.NPeano.
 Require Coq.Lists.List.
 
 Local Close Scope nat_scope. Local Close Scope type_scope. Local Close Scope core_scope.
diff --git a/src/Arithmetic/ModularArithmeticTheorems.v b/src/Arithmetic/ModularArithmeticTheorems.v
index 1fd33881b3..835aba5af9 100644
--- a/src/Arithmetic/ModularArithmeticTheorems.v
+++ b/src/Arithmetic/ModularArithmeticTheorems.v
@@ -176,7 +176,7 @@ Module F.
     Qed.
   End FandZ.
   Section FandNat.
-    Import NPeano Nat.
+    Import Nat.
     Local Infix "mod" := modulo : nat_scope.
     Local Open Scope nat_scope.
 
diff --git a/src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Proofs.v b/src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Proofs.v
index 6191a836a1..fd22363581 100644
--- a/src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Proofs.v
+++ b/src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Proofs.v
@@ -89,7 +89,7 @@ Section WordByWordMontgomery.
        numlimbs_drop_high
        using (repeat autounfold with word_by_word_montgomery; t_small)
     : push_numlimbs.
-  Hint Rewrite <- Max.succ_max_distr pred_Sn Min.succ_min_distr : push_numlimbs.
+  Hint Rewrite <- Nat.succ_max_distr pred_Sn Nat.succ_min_distr : push_numlimbs.
 
 
   (* Recurse for a as many iterations as A has limbs, varying A := A, S := 0, r, bounds *)
@@ -167,7 +167,7 @@ Section WordByWordMontgomery.
       repeat autounfold with word_by_word_montgomery; rewrite Z.mul_split_mod.
       repeat autorewrite with push_numlimbs.
       change Init.Nat.max with Nat.max.
-      rewrite <- ?(Max.max_assoc (numlimbs S)).
+      rewrite <- ?(Nat.max_assoc (numlimbs S)).
       reflexivity.
     Qed.
 
@@ -326,11 +326,11 @@ Section WordByWordMontgomery.
   Local Ltac t_min_max_step _ :=
     match goal with
     | [ |- context[Init.Nat.max ?x ?y] ]
-      => first [ rewrite (Max.max_l x y) by lia
-               | rewrite (Max.max_r x y) by lia ]
+      => first [ rewrite (Nat.max_l x y) by lia
+               | rewrite (Nat.max_r x y) by lia ]
     | [ |- context[Init.Nat.min ?x ?y] ]
-      => first [ rewrite (Min.min_l x y) by lia
-               | rewrite (Min.min_r x y) by lia ]
+      => first [ rewrite (Nat.min_l x y) by lia
+               | rewrite (Nat.min_r x y) by lia ]
     | _ => progress change Init.Nat.max with Nat.max
     | _ => progress change Init.Nat.min with Nat.min
     end.
@@ -364,7 +364,7 @@ Section WordByWordMontgomery.
                      | rewrite Nat.min_comm, Nat.min_max_distr ]. }
     rewrite Hgen; clear Hgen.
     destruct count; [ reflexivity | ].
-    repeat apply Max.max_case_strong; apply Min.min_case_strong; lia.
+    repeat apply Nat.max_case_strong; apply Nat.min_case_strong; lia.
   Qed.
 
 
diff --git a/src/Compilers/Named/NameUtilProperties.v b/src/Compilers/Named/NameUtilProperties.v
index 6f124b0fe7..4c3e3478ca 100644
--- a/src/Compilers/Named/NameUtilProperties.v
+++ b/src/Compilers/Named/NameUtilProperties.v
@@ -71,7 +71,7 @@ Section language.
       unfold mname_list_unique; intro H; split; intros k N;
         rewrite <- ?firstn_map, <- ?skipn_map, ?skipn_skipn, ?firstn_firstn_min, ?firstn_skipn_add;
         intros; eapply H; try eassumption.
-      { apply Min.min_case_strong.
+      { apply Nat.min_case_strong.
         { match goal with H : _ |- _ => rewrite skipn_firstn in H end;
             eauto using In_firstn. }
         { intro; match goal with H : _ |- _ => rewrite skipn_all in H by (rewrite firstn_length; lia * ) end.
diff --git a/src/Compilers/WfReflectiveGen.v b/src/Compilers/WfReflectiveGen.v
index 2a89bbd61a..33bc1eade4 100644
--- a/src/Compilers/WfReflectiveGen.v
+++ b/src/Compilers/WfReflectiveGen.v
@@ -240,14 +240,14 @@ Section language.
     : fst (natize_interp_flat_type base v1) = length (flatten_binding_list v1 v2) + base.
   Proof using Type.
     revert base; induction t; simpl; [ reflexivity | reflexivity | ].
-    intros; rewrite List.app_length, <- plus_assoc.
+    intros; rewrite List.app_length, <- Nat.add_assoc.
     rewrite_hyp <- ?*; reflexivity.
   Qed.
   Lemma length_natize_interp_flat_type2 {t} (base : nat) (v1 : interp_flat_type var1 t) (v2 : interp_flat_type var2 t)
     : fst (natize_interp_flat_type base v2) = length (flatten_binding_list v1 v2) + base.
   Proof using Type.
     revert base; induction t; simpl; [ reflexivity | reflexivity | ].
-    intros; rewrite List.app_length, <- plus_assoc.
+    intros; rewrite List.app_length, <- Nat.add_assoc.
     rewrite_hyp <- ?*; reflexivity.
   Qed.
 
@@ -285,7 +285,7 @@ Section language.
        | TT, TT => rTrue
        | TT, _ => rFalse
        | Var t0 x, Var t1 y
-         => match beq_nat (fst x) (fst y), List.nth_error G (List.length G - S (fst x)) with
+         => match Nat.eqb (fst x) (fst y), List.nth_error G (List.length G - S (fst x)) with
            | true, Some v => eq_type_and_var v (existT _ (t0, t1) (snd x, snd y))
            | _, _ => rFalse
            end
diff --git a/src/Compilers/Z/Bounds/RoundUpLemmas.v b/src/Compilers/Z/Bounds/RoundUpLemmas.v
index 1831fe379d..bd7da9c11c 100644
--- a/src/Compilers/Z/Bounds/RoundUpLemmas.v
+++ b/src/Compilers/Z/Bounds/RoundUpLemmas.v
@@ -1,4 +1,5 @@
 Require Import Coq.micromega.Lia Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop.
+Require Import Coq.Arith.PeanoNat.
 Require Import Crypto.Compilers.Z.Bounds.Interpretation.
 Require Import Crypto.Util.ZRange.
 Require Import Crypto.Util.Tactics.BreakMatch.
@@ -27,8 +28,8 @@ Proof.
            | _ => progress simpl in *
            | _ => progress break_innermost_match_step
            | _ => progress break_innermost_match_hyps_step
-           | [ H : ?leb _ _ = true |- _ ] => apply NPeano.Nat.leb_le in H
-           | [ H : ?leb _ _ = false |- _ ] => apply NPeano.Nat.leb_gt in H
+           | [ H : ?leb _ _ = true |- _ ] => apply Nat.leb_le in H
+           | [ H : ?leb _ _ = false |- _ ] => apply Nat.leb_gt in H
            | _ => lia *
            end. }
 Qed.
diff --git a/src/Experiments/SimplyTypedArithmetic.v b/src/Experiments/SimplyTypedArithmetic.v
index 22578935aa..3ff29fb5f0 100644
--- a/src/Experiments/SimplyTypedArithmetic.v
+++ b/src/Experiments/SimplyTypedArithmetic.v
@@ -7385,7 +7385,7 @@ Section rcarry_mul.
       rewrite negb_false_iff in *.
       Z.ltb_to_lt.
       rewrite Qle_bool_iff in *.
-      rewrite NPeano.Nat.eqb_neq in *.
+      rewrite Nat.eqb_neq in *.
       intros.
       cbv [Qnum Qden limbwidth Qceiling Qfloor Qopp Qdiv Qplus inject_Z Qmult Qinv] in *.
       rewrite ?map_length, ?Z.mul_0_r, ?Pos.mul_1_r, ?Z.mul_1_r in *.
diff --git a/src/LegacyArithmetic/BaseSystem.v b/src/LegacyArithmetic/BaseSystem.v
index 59299d6dba..7893bf11d7 100644
--- a/src/LegacyArithmetic/BaseSystem.v
+++ b/src/LegacyArithmetic/BaseSystem.v
@@ -1,6 +1,6 @@
 Require Import Coq.Lists.List.
 Require Import Coq.ZArith.ZArith Coq.ZArith.Zdiv.
-Require Import Coq.micromega.Lia Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop Coq.Numbers.Natural.Peano.NPeano Coq.Arith.Arith.
+Require Import Coq.micromega.Lia Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop Coq.Arith.Arith.
 Require Import Crypto.Util.ListUtil.
 Require Import Crypto.Util.Notations.
 Require Export Crypto.Util.FixCoqMistakes.
diff --git a/src/LegacyArithmetic/BaseSystemProofs.v b/src/LegacyArithmetic/BaseSystemProofs.v
index a4e33325c1..2b7bc27991 100644
--- a/src/LegacyArithmetic/BaseSystemProofs.v
+++ b/src/LegacyArithmetic/BaseSystemProofs.v
@@ -1,7 +1,7 @@
 Require Import Coq.Lists.List Coq.micromega.Psatz Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop.
 Require Import Crypto.Util.ListUtil.
 Require Import Coq.ZArith.ZArith Coq.ZArith.Zdiv.
-Require Import Coq.micromega.Lia Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop Coq.Numbers.Natural.Peano.NPeano Coq.Arith.Arith.
+Require Import Coq.micromega.Lia Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop Coq.Arith.Arith.
 Require Import Crypto.LegacyArithmetic.BaseSystem.
 Require Import Crypto.Util.Tactics.UniquePose.
 Require Import Crypto.Util.Notations.
@@ -101,7 +101,7 @@ Section BaseSystemProofs.
   Qed.
   Hint Rewrite peel_decode.
 
-  Hint Rewrite plus_0_r.
+  Hint Rewrite Nat.add_0_r.
 
   Lemma set_higher : forall bs vs x,
     decode' bs (vs++x::nil) = decode' bs vs + nth_default 0 bs (length vs) * x.
@@ -128,7 +128,7 @@ Section BaseSystemProofs.
       assert (HH: nth_error (z0 :: l) 0 = Some z) by
           (
             pose proof @nth_error_skipn _ (length vs) bs 0;
-            rewrite plus_0_r in *;
+            rewrite Nat.add_0_r in *;
             congruence); simpl in HH; congruence. }
   Qed.
 End BaseSystemProofs.
diff --git a/src/LegacyArithmetic/Pow2BaseProofs.v b/src/LegacyArithmetic/Pow2BaseProofs.v
index a1aa8585e3..a0b58a9a00 100644
--- a/src/LegacyArithmetic/Pow2BaseProofs.v
+++ b/src/LegacyArithmetic/Pow2BaseProofs.v
@@ -1,6 +1,5 @@
 Require Import Coq.Classes.RelationClasses Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop.
 Require Import Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.micromega.Psatz Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop.
-Require Import Coq.Numbers.Natural.Peano.NPeano.
 Require Import Coq.Lists.List.
 Require Import Coq.funind.Recdef.
 Require Import Crypto.Util.ListUtil Crypto.Util.NatUtil.
@@ -116,7 +115,7 @@ Section Pow2BaseProofs.
       erewrite base_from_limb_widths_step; eauto.
       f_equal.
       simpl.
-      destruct (NPeano.Nat.eq_dec i 0).
+      destruct (Nat.eq_dec i 0).
       - subst; unfold sum_firstn; simpl.
         apply nth_error_exists_first in nth_err_w.
         destruct nth_err_w as [l' lw_destruct]; subst.
@@ -162,7 +161,7 @@ Section Pow2BaseProofs.
     autorewrite with simpl_firstn simpl_skipn in *.
     rewrite H, skipn_app, skipn_all by auto with arith distr_length; clear H.
     simpl; distr_length.
-    apply Min.min_case_strong; intro;
+    apply Nat.min_case_strong; intro;
       unfold sum_firstn; autorewrite with natsimplify simpl_skipn simpl_firstn;
         reflexivity.
   Qed.
diff --git a/src/Primitives/EdDSARepChange.v b/src/Primitives/EdDSARepChange.v
index 07d370b26e..9ef9601dda 100644
--- a/src/Primitives/EdDSARepChange.v
+++ b/src/Primitives/EdDSARepChange.v
@@ -12,7 +12,6 @@ Require Import Coq.micromega.Lia Coq.Classes.Morphisms Coq.Classes.Morphisms_Pro
 Require Import Crypto.Util.Notations.
 Require Import Crypto.Util.Option Crypto.Util.Logic Crypto.Util.Relations Crypto.Util.WordUtil Util.LetIn Util.NatUtil.
 Require Import Crypto.Spec.ModularArithmetic Crypto.Arithmetic.PrimeFieldTheorems.
-Import NPeano.
 
 Import Notations.
 
diff --git a/src/Spec/EdDSA.v b/src/Spec/EdDSA.v
index d163ab4fd9..fc519b872a 100644
--- a/src/Spec/EdDSA.v
+++ b/src/Spec/EdDSA.v
@@ -2,7 +2,6 @@ Require bbv.WordScope Crypto.Util.WordUtil.
 Require Import Coq.ZArith.BinIntDef.
 Require Crypto.Algebra.Hierarchy Algebra.ScalarMult.
 Require Coq.ZArith.Znumtheory Coq.ZArith.BinInt.
-Require Coq.Numbers.Natural.Peano.NPeano.
 
 Require Import Crypto.Spec.ModularArithmetic.
 
diff --git a/src/Util/Decidable/Decidable2Bool.v b/src/Util/Decidable/Decidable2Bool.v
index 138051d88e..5a6455414d 100644
--- a/src/Util/Decidable/Decidable2Bool.v
+++ b/src/Util/Decidable/Decidable2Bool.v
@@ -37,7 +37,7 @@ Lemma dec_nat_eq_to_bool a b
   : (if dec (a = b) then true else false) = Nat.eqb a b.
 Proof.
   destruct (Nat.eqb a b) eqn:H; break_match; try reflexivity.
-  { apply beq_nat_true in H; congruence. }
+  { apply Nat.eqb_eq in H; congruence. }
   { rewrite Nat.eqb_refl in H; congruence. }
 Qed.
 #[global]
diff --git a/src/Util/FixedWordSizesEquality.v b/src/Util/FixedWordSizesEquality.v
index ead247caed..e56c613f37 100644
--- a/src/Util/FixedWordSizesEquality.v
+++ b/src/Util/FixedWordSizesEquality.v
@@ -31,7 +31,7 @@ Proof.
   destruct (NatUtil.nat_eq_dec x y) as [pf|pf]; [ intros; assumption | ].
   intro H; exfalso.
   let pf := pf in
-  abstract (apply pf; eapply NPeano.Nat.pow_inj_r; [ | eassumption ]; lia).
+  abstract (apply pf; eapply Nat.pow_inj_r; [ | eassumption ]; lia).
 Defined.
 Lemma pow2_inj_helper_refl x p : pow2_inj_helper x x p = eq_refl.
 Proof.
diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v
index a54878ffbf..eda4534525 100644
--- a/src/Util/ListUtil.v
+++ b/src/Util/ListUtil.v
@@ -4,7 +4,6 @@ Require Import Coq.ZArith.ZArith.
 Require Import Coq.micromega.Lia Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop.
 Require Import Coq.Arith.Peano_dec.
 Require Import Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop.
-Require Import Coq.Numbers.Natural.Peano.NPeano.
 Require Import Crypto.Util.NatUtil.
 Require Import Crypto.Util.Pointed.
 Require Import Crypto.Util.Prod.
@@ -172,10 +171,10 @@ Module Export List.
   Proof.
    revert start. induction len as [|len IHlen]; simpl; intros.
    - rewrite <- plus_n_O. split;[easy|].
-     intros (H,H'). apply (Lt.lt_irrefl _ (Lt.le_lt_trans _ _ _ H H')).
+     intros (H,H'). apply (Nat.lt_irrefl _ (Nat.le_lt_trans _ _ _ H H')).
    - rewrite IHlen, <- plus_n_Sm; simpl; split.
      * intros [H|H]; subst; intuition auto with arith.
-     * intros (H,H'). destruct (Lt.le_lt_or_eq _ _ H); intuition.
+     * intros (H,H'). destruct (proj1 (Nat.lt_eq_cases _ _) H); intuition.
   Qed.
 
   Section Facts.
@@ -226,7 +225,7 @@ Module Export List.
     Lemma firstn_length_le: forall l:list A, forall n:nat,
           n <= length l -> length (firstn n l) = n.
     Proof using Type. induction l as [|x xs Hrec].
-           - simpl. intros n H. apply le_n_0_eq in H. rewrite <- H. now simpl.
+           - simpl. intros n H. apply Nat.le_0_r in H. rewrite H. now simpl.
            - destruct n as [|n].
              * now simpl.
              * simpl. intro H. apply le_S_n in H. now rewrite (Hrec n H).
@@ -238,7 +237,7 @@ Module Export List.
     Proof using Type. induction n as [|k iHk]; intros l1 l2.
            - now simpl.
            - destruct l1 as [|x xs].
-             * unfold List.firstn at 2, length. now rewrite 2!app_nil_l, <- minus_n_O.
+             * unfold List.firstn at 2, length. now rewrite 2!app_nil_l, Nat.sub_0_r.
              * rewrite <- app_comm_cons. simpl. f_equal. apply iHk.
     Qed.
 
@@ -247,7 +246,7 @@ Module Export List.
         firstn ((length l1) + n) (l1 ++ l2) = l1 ++ firstn n l2.
     Proof using Type. induction n as [| k iHk];intros l1 l2.
            - unfold List.firstn at 2. rewrite <- plus_n_O, app_nil_r.
-             rewrite firstn_app. rewrite <- minus_diag_reverse.
+             rewrite firstn_app. rewrite Nat.sub_diag.
              unfold List.firstn at 2. rewrite app_nil_r. apply firstn_all.
            - destruct l2 as [|x xs].
              * simpl. rewrite app_nil_r. apply firstn_all2. auto with arith.
@@ -1360,7 +1359,7 @@ Lemma firstn_firstn : forall {A} m n (l : list A), (n <= m)%nat ->
   firstn n (firstn m l) = firstn n l.
 Proof.
   intros A m n l H; rewrite firstn_firstn_min.
-  apply Min.min_case_strong; intro; [ reflexivity | ].
+  apply Nat.min_case_strong; intro; [ reflexivity | ].
   assert (n = m) by lia; subst; reflexivity.
 Qed.
 
@@ -1874,7 +1873,7 @@ Proof.
   intros A d l i; induction n as [|n IHn]; break_match; autorewrite with push_nth_default; auto; try lia.
   + rewrite (firstn_succ d) by lia.
     autorewrite with push_nth_default; repeat (break_match_hyps; break_match; distr_length);
-      rewrite Min.min_l in * by lia; try lia.
+      rewrite Nat.min_l in * by lia; try lia.
     - apply IHn; lia.
     - replace i with n in * by lia.
       rewrite Nat.sub_diag.
diff --git a/src/Util/NUtil.v b/src/Util/NUtil.v
index a0145739f1..b14356053e 100644
--- a/src/Util/NUtil.v
+++ b/src/Util/NUtil.v
@@ -1,6 +1,5 @@
 Require Import Coq.Classes.RelationClasses Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop.
 Require Import Coq.NArith.NArith.
-Require Import Coq.Numbers.Natural.Peano.NPeano.
 Require Import Crypto.Util.NatUtil Crypto.Util.Decidable.
 Require Export Crypto.Util.NUtil.WithoutReferenceToZ.
 Require bbv.WordScope.
diff --git a/src/Util/NUtil/WithoutReferenceToZ.v b/src/Util/NUtil/WithoutReferenceToZ.v
index 5178df48eb..166808c63b 100644
--- a/src/Util/NUtil/WithoutReferenceToZ.v
+++ b/src/Util/NUtil/WithoutReferenceToZ.v
@@ -1,8 +1,7 @@
 (** NUtil that doesn't depend on ZUtil stuff *)
 (** Should probably come up with a better organization of this stuff *)
 Require Import Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop Coq.Classes.RelationClasses.
-Require Import Coq.NArith.NArith.
-Require Import Coq.Numbers.Natural.Peano.NPeano.
+Require Import Coq.NArith.NArith Coq.Arith.PeanoNat.
 Require Import Crypto.Util.NatUtil Crypto.Util.Decidable.
 
 Module N.
diff --git a/src/Util/NatUtil.v b/src/Util/NatUtil.v
index 1452432f04..4b73f8ade4 100644
--- a/src/Util/NatUtil.v
+++ b/src/Util/NatUtil.v
@@ -1,5 +1,5 @@
 Require Coq.Logic.Eqdep_dec.
-Require Import Coq.Numbers.Natural.Peano.NPeano Coq.micromega.Lia Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop.
+Require Import Coq.micromega.Lia Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop.
 Require Import Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop.
 Require Import Coq.Relations.Relation_Definitions.
 Require Import Coq.micromega.Lia Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop.
@@ -16,8 +16,7 @@ Global Existing Instance Nat.le_preorder.
 Global Hint Resolve Nat.max_l Nat.max_r Nat.le_max_l Nat.le_max_r: arith.
 Global Hint Resolve Nat.min_l Nat.min_r Nat.le_min_l Nat.le_min_r: arith.
 
-
-Global Hint Resolve mod_bound_pos plus_le_compat : arith.
+Global Hint Resolve mod_bound_pos Nat.add_le_mono : arith.
 Global Hint Resolve (fun x y p q => proj1 (@Nat.mod_bound_pos x y p q)) (fun x y p q => proj2 (@Nat.mod_bound_pos x y p q)) : arith.
 
 #[global]
@@ -29,9 +28,9 @@ Hint Rewrite sub_diag add_0_l add_0_r sub_0_r sub_succ : natsimplify.
 Local Open Scope nat_scope.
 
 Lemma min_def {x y} : min x y = x - (x - y).
-Proof. apply Min.min_case_strong; lia. Qed.
+Proof. apply Nat.min_case_strong; lia. Qed.
 Lemma max_def {x y} : max x y = x + (y - x).
-Proof. apply Max.max_case_strong; lia. Qed.
+Proof. apply Nat.max_case_strong; lia. Qed.
 Ltac coq_lia := lia.
 Ltac handle_min_max_for_lia_gen min max :=
   repeat match goal with
@@ -44,8 +43,8 @@ Ltac handle_min_max_for_lia_case_gen min max :=
   repeat match goal with
          | [ H : context[min _ _] |- _ ] => revert H
          | [ H : context[max _ _] |- _ ] => revert H
-         | [ |- context[min _ _] ] => apply Min.min_case_strong
-         | [ |- context[max _ _] ] => apply Max.max_case_strong
+         | [ |- context[min _ _] ] => apply Nat.min_case_strong
+         | [ |- context[max _ _] ] => apply Nat.max_case_strong
          end;
   intros.
 Ltac handle_min_max_for_lia := handle_min_max_for_lia_gen min max.
@@ -173,7 +172,7 @@ Proof.
     rewrite H1.
     exists 0; auto.
   } {
-    rewrite mult_succ_r in H1.
+    rewrite Nat.mul_succ_r in H1.
     assert (4 <= x) as le4x by (apply Nat.div_str_pos_iff; lia).
     rewrite <- Nat.add_1_r in H.
     replace x with ((x - 4) + 4) in H by lia.
@@ -224,11 +223,11 @@ Proof.
 Qed.
 
 Lemma beq_nat_eq_nat_dec {R} (x y : nat) (a b : R)
-  : (if EqNat.beq_nat x y then a else b) = (if eq_nat_dec x y then a else b).
+  : (if Nat.eqb x y then a else b) = (if eq_nat_dec x y then a else b).
 Proof.
   destruct (eq_nat_dec x y) as [H|H];
-    [ rewrite (proj2 (@beq_nat_true_iff _ _) H); reflexivity
-    | rewrite (proj2 (@beq_nat_false_iff _ _) H); reflexivity ].
+    [ rewrite (proj2 (@Nat.eqb_eq _ _) H); reflexivity
+    | rewrite (proj2 (@Nat.eqb_neq _ _) H); reflexivity ].
 Qed.
 
 Lemma pow_nonzero a k : a <> 0 -> a ^ k <> 0.
@@ -325,7 +324,7 @@ Qed.
 Hint Rewrite eq_nat_dec_n_S : natsimplify.
 
 #[global]
-Hint Rewrite Max.max_0_l Max.max_0_r Max.max_idempotent Min.min_0_l Min.min_0_r Min.min_idempotent : natsimplify.
+Hint Rewrite Nat.max_0_l Nat.max_0_r Nat.max_idempotent Nat.min_0_l Nat.min_0_r Nat.min_idempotent : natsimplify.
 
 (** Helper to get around the lack of function extensionality *)
 Definition le_dec_right_val n m (pf0 : ~n <= m) : { pf | le_dec n m = right pf }.
@@ -403,15 +402,15 @@ Lemma setbit_high : forall x i, (x < 2^i -> setbit x i = x + 2^i)%nat.
 Proof.
   intros x i H; apply bits_inj; intro n.
   rewrite setbit_eqb.
-  destruct (beq_nat i n) eqn:H'; simpl.
-  { apply beq_nat_true in H'; subst.
+  destruct (Nat.eqb i n) eqn:H'; simpl.
+  { apply Nat.eqb_eq in H'; subst.
     symmetry; apply testbit_true.
     rewrite div_minus, div_small by lia.
     reflexivity. }
   { assert (H'' : (((x + 2 ^ i) / 2 ^ n) mod 2) = ((x / 2 ^ n) mod 2)).
     { assert (2^(i-n) <> 0) by auto with arith.
       assert (2^(i-n) <> 0) by lia.
-      destruct (lt_eq_lt_dec i n) as [ [?|?] | ? ]; [ | subst; rewrite <- beq_nat_refl in H'; congruence | ].
+      destruct (lt_eq_lt_dec i n) as [ [?|?] | ? ]; [ | subst; rewrite Nat.eqb_refl in H'; congruence | ].
       { assert (i <= n - 1) by lia.
         assert (2^i <= 2^n) by auto using pow_le_mono_r with arith.
         assert (2^i <= 2^(n - 1)) by auto using pow_le_mono_r with arith.
@@ -474,7 +473,7 @@ Module Export Hints.
   Global Existing Instance Nat.le_preorder.
   Global Hint Resolve Nat.max_l Nat.max_r Nat.le_max_l Nat.le_max_r: arith.
   Global Hint Resolve Nat.min_l Nat.min_r Nat.le_min_l Nat.le_min_r: arith.
-  Global Hint Resolve mod_bound_pos plus_le_compat : arith.
+  Global Hint Resolve mod_bound_pos Nat.add_le_mono : arith.
   Global Hint Resolve (fun x y p q => proj1 (@Nat.mod_bound_pos x y p q)) (fun x y p q => proj2 (@Nat.mod_bound_pos x y p q)) : arith.
 #[global]
   Hint Rewrite @mod_small @mod_mod @mod_1_l @mod_1_r succ_pred using lia : natsimplify.
@@ -504,7 +503,7 @@ Module Export Hints.
 #[global]
   Hint Rewrite eq_nat_dec_n_S : natsimplify.
 #[global]
-  Hint Rewrite Max.max_0_l Max.max_0_r Max.max_idempotent Min.min_0_l Min.min_0_r Min.min_idempotent : natsimplify.
+  Hint Rewrite Nat.max_0_l Nat.max_0_r Nat.max_idempotent Nat.min_0_l Nat.min_0_r Nat.min_idempotent : natsimplify.
 #[global]
   Hint Rewrite lt_dec_irrefl : natsimplify.
 #[global]
diff --git a/src/Util/NumTheoryUtil.v b/src/Util/NumTheoryUtil.v
index a095929db3..215f5663ce 100644
--- a/src/Util/NumTheoryUtil.v
+++ b/src/Util/NumTheoryUtil.v
@@ -1,5 +1,5 @@
 Require Import Coq.ZArith.Zpower Coq.ZArith.Znumtheory Coq.ZArith.ZArith Coq.ZArith.Zdiv.
-Require Import Coq.Bool.Bool Coq.micromega.Lia Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop Coq.Numbers.Natural.Peano.NPeano Coq.Arith.Arith.
+Require Import Coq.Bool.Bool Coq.micromega.Lia Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop Coq.Arith.Arith.
 Require Import Coq.Classes.RelationClasses Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop.
 Require Import Crypto.Util.ZUtil.Divide.
 Require Import Crypto.Util.ZUtil.Modulo.
diff --git a/src/Util/Strings/String.v b/src/Util/Strings/String.v
index d43d8952ec..5a33559985 100644
--- a/src/Util/Strings/String.v
+++ b/src/Util/Strings/String.v
@@ -1,4 +1,4 @@
-Require Import Coq.micromega.Lia Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop.
+Require Import Coq.micromega.Lia Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop Coq.Arith.PeanoNat.
 Require Import Coq.Strings.String.
 Require Import Coq.Strings.Ascii.
 Require Import Crypto.Util.Strings.Equality.
@@ -114,7 +114,7 @@ Lemma length_substring n1 n2 s
 Proof.
   revert n1 n2; induction s as [|a s IHs]; intros; cbn.
   { destruct n1, n2; cbn; reflexivity. }
-  { destruct n1; [ destruct n2 | ]; cbn; rewrite ?IHs, <- ?Minus.minus_n_O; reflexivity. }
+  { destruct n1; [ destruct n2 | ]; cbn; rewrite ?IHs, ?Nat.sub_0_r; reflexivity. }
 Qed.
 
 Lemma length_append s1 s2 : length (s1 ++ s2) = length s1 + length s2.
diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v
index 7010381e19..2431be73b6 100644
--- a/src/Util/Tuple.v
+++ b/src/Util/Tuple.v
@@ -1,5 +1,6 @@
 Require Import Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop.
 Require Import Coq.Relations.Relation_Definitions.
+Require Import Coq.Arith.PeanoNat.
 Require Import Coq.Lists.List.
 Require Import Coq.micromega.Lia Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop.
 Require Import Crypto.Util.Option.
@@ -258,7 +259,7 @@ Definition on_tuple2 {A B C} (f : list A -> list B -> list C) {a b c : nat}
                (Hlength (to_list a ta) (to_list b tb) (length_to_list ta) (length_to_list tb)).
 
 Definition map2 {n A B C} (f:A -> B -> C) (xs:tuple A n) (ys:tuple B n) : tuple C n
-  := on_tuple2 (map2 f) (fun la lb pfa pfb => eq_trans (@map2_length _ _ _ _ la lb) (eq_trans (f_equal2 _ pfa pfb) (Min.min_idempotent _))) xs ys.
+  := on_tuple2 (map2 f) (fun la lb pfa pfb => eq_trans (@map2_length _ _ _ _ la lb) (eq_trans (f_equal2 _ pfa pfb) (Nat.min_idempotent _))) xs ys.
 
 Lemma to_list'_ext {n A} (xs ys:tuple' A n) : to_list' n xs = to_list' n ys -> xs = ys.
 Proof.
diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v
index 3f1bdabe7a..8430269fd2 100644
--- a/src/Util/WordUtil.v
+++ b/src/Util/WordUtil.v
@@ -1,9 +1,8 @@
-Require Import Coq.Numbers.Natural.Peano.NPeano.
 Require Import Coq.ZArith.ZArith.
 Require Import Coq.NArith.NArith.
 Require Import Coq.Classes.RelationClasses Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop.
 Require Import Coq.Program.Program.
-Require Import Coq.Numbers.Natural.Peano.NPeano Util.NatUtil.
+Require Import Util.NatUtil.
 Require Import Coq.micromega.Psatz Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop.
 Require Import Coq.Bool.Bool.
 
@@ -817,7 +816,7 @@ Module Export Hints4.
   Hint Rewrite @wordToN_cast_word : push_wordToN.
 End Hints4.
 
-Import NPeano Nat.
+Import Nat.
 Local Infix "++" := combine.
 
 Definition zext_ge n {m} {pf:m <= n} (w:word m) : word n :=
@@ -897,7 +896,7 @@ Proof.
            => progress change min' with min
          end.
   generalize (split1 _ _ x); generalize (split2 _ _ x); clear x; simpl.
-  apply Min.min_case_strong; intros Hbc x0 x1;
+  apply Nat.min_case_strong; intros Hbc x0 x1;
     pose proof (wordToNat_bound x0); pose proof (wordToNat_bound x1).
   { assert (b - c = 0) by lia.
     assert (2^b <= 2^c) by auto using pow_le_mono_r with arith.
@@ -928,7 +927,7 @@ Proof.
   rewrite <- (combine_split _ _ x) at 2.
   rewrite wand_combine, !wordToNat_combine, wand_kill, wand_unit, wordToNat_wzero.
   generalize (split1 _ _ x); generalize (split2 _ _ x); clear x; simpl.
-  apply Min.min_case_strong; intros Hbc x0 x1;
+  apply Nat.min_case_strong; intros Hbc x0 x1;
     pose proof (wordToNat_bound x0); pose proof (wordToNat_bound x1).
   { assert (b - c = 0) by lia.
     assert (2^b <= 2^c) by auto using pow_le_mono_r with arith.
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index f496ea2327..7c4422d9f7 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -1,5 +1,5 @@
 Require Coq.ZArith.Zpower Coq.ZArith.Znumtheory Coq.ZArith.ZArith Coq.ZArith.Zdiv.
-Require Coq.micromega.Lia Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop Coq.micromega.Psatz Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop Coq.Numbers.Natural.Peano.NPeano Coq.Arith.Arith.
+Require Coq.micromega.Lia Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop Coq.micromega.Psatz Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop Coq.Arith.Arith.
 Require Crypto.Util.ZUtil.AddGetCarry.
 Require Crypto.Util.ZUtil.AddModulo.
 Require Crypto.Util.ZUtil.CC.
diff --git a/src/Util/ZUtil/Hints/Core.v b/src/Util/ZUtil/Hints/Core.v
index ff666e0adb..08c443ace7 100644
--- a/src/Util/ZUtil/Hints/Core.v
+++ b/src/Util/ZUtil/Hints/Core.v
@@ -112,6 +112,7 @@ Module Coq.
     End PreOmega.
   End omega.
 End Coq.
+
 Ltac Coq.omega.PreOmega.zify_nat_op ::=
  match goal with
   (* misc type conversions: positive/N/Z to nat *)
@@ -139,8 +140,8 @@ Ltac Coq.omega.PreOmega.zify_nat_op ::=
   | |- context [ Z.of_nat (minus ?a ?b) ] => rewrite (Nat2Z.inj_sub_max a b)
 
   (* pred -> minus ... -1 -> Z.max (Z.sub ... -1) 0 *)
-  | H : context [ Z.of_nat (pred ?a) ] |- _ => rewrite (pred_of_minus a) in H
-  | |- context [ Z.of_nat (pred ?a) ] => rewrite (pred_of_minus a)
+ | H : context [ Z.of_nat (pred ?a) ] |- _ => rewrite <-(Nat.sub_1_r a) in H
+ | |- context [ Z.of_nat (pred ?a) ] => rewrite <-(Nat.sub_1_r a)
 
   (* mult -> Z.mul and a positivity hypothesis *)
   | H : context [ Z.of_nat (mult ?a ?b) ] |- _ =>
diff --git a/src/Util/ZUtil/Shift.v b/src/Util/ZUtil/Shift.v
index cd9cc0b7e5..9a8e8e5bf4 100644
--- a/src/Util/ZUtil/Shift.v
+++ b/src/Util/ZUtil/Shift.v
@@ -216,13 +216,13 @@ Module Z.
     rewrite Z.shiftl_mul_pow2 by apply Nat2Z.is_nonneg.
     replace (b * 2 ^ Z.of_nat n) with
       ((b * 2 ^ Z.of_nat (n - m)) * 2 ^ Z.of_nat m) by
-      (rewrite (le_plus_minus m n) at 2; try assumption;
-       rewrite Nat2Z.inj_add, Z.pow_add_r by apply Nat2Z.is_nonneg; ring).
+        (rewrite <-(Nat.sub_add m n H) at 2;
+         rewrite Nat2Z.inj_add, Z.pow_add_r by apply Nat2Z.is_nonneg; ring).
     rewrite Z.mod_add by (pose proof (Z.pow_pos_nonneg 2 (Z.of_nat m)); lia).
     symmetry. apply Znumtheory.Zmod_div_mod; try (apply Z.pow_pos_nonneg; lia).
-    rewrite (le_plus_minus m n) by assumption.
+    rewrite <-(Nat.sub_add m n) by assumption.
     rewrite Nat2Z.inj_add, Z.pow_add_r by apply Nat2Z.is_nonneg.
-    apply Z.divide_factor_l.
+    now rewrite Z.mul_comm; apply Z.divide_factor_l.
   Qed.
 
   Lemma shiftl_add x y z : 0 <= z -> (x + y) << z = (x << z) + (y << z).