diff --git a/src/AbstractInterpretation/Wf.v b/src/AbstractInterpretation/Wf.v
index 87942c42c0..3f3cc70107 100644
--- a/src/AbstractInterpretation/Wf.v
+++ b/src/AbstractInterpretation/Wf.v
@@ -715,8 +715,8 @@ Module Compilers.
                            | break_innermost_match_hyps_step
                            | congruence
                            | rewrite List.combine_length in *
-                           | rewrite NPeano.Nat.min_r in * by lia
-                           | rewrite NPeano.Nat.min_l in * by lia
+                           | rewrite Nat.min_r in * by lia
+                           | rewrite Nat.min_l in * by lia
                            | progress expr.inversion_wf_one_constr
                            | progress expr.invert_match
                            | match goal with
diff --git a/src/Algebra/Hierarchy.v b/src/Algebra/Hierarchy.v
index 07f1f30fd9..8b1fd2eeb9 100644
--- a/src/Algebra/Hierarchy.v
+++ b/src/Algebra/Hierarchy.v
@@ -4,7 +4,6 @@ Require Export Crypto.Util.Decidable.
 Require Coq.PArith.BinPos.
 Require Import Coq.Classes.Morphisms.
 
-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/Core.v b/src/Arithmetic/Core.v
index c46d4b2a02..4ee559970d 100644
--- a/src/Arithmetic/Core.v
+++ b/src/Arithmetic/Core.v
@@ -858,8 +858,8 @@ Module Positional.
     destruct (dec (i < S n)%nat);
       break_innermost_match; cbn [fst snd] in *; Z.ltb_to_lt; [ | rewrite IHn | | rewrite IHn ];
         break_innermost_match;
-        rewrite ?Min.min_l in * by lia;
-        rewrite ?Min.min_r in * by lia;
+        rewrite ?Nat.min_l in * by lia;
+        rewrite ?Nat.min_r in * by lia;
         eauto with lia.
     { rewrite weight_mul_iff in * by auto.
       destruct_head'_or; try lia.
diff --git a/src/Arithmetic/ModularArithmeticTheorems.v b/src/Arithmetic/ModularArithmeticTheorems.v
index 799fc2e477..9d9bb6f5f7 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/SolinasReduction.v b/src/Arithmetic/SolinasReduction.v
index 07e8a94b77..07bcbead50 100644
--- a/src/Arithmetic/SolinasReduction.v
+++ b/src/Arithmetic/SolinasReduction.v
@@ -1110,7 +1110,7 @@ Module SolinasReduction.
       weight x1 <= weight x2.
     Proof using Type.
       intros H.
-      apply le_lt_or_eq in H.
+      apply Nat.lt_eq_cases in H.
       intuition.
       pose proof (weight_mono x1 x2 ltac:(auto)); lia.
       subst; lia.
diff --git a/src/Bedrock/Field/Synthesis/Generic/Bignum.v b/src/Bedrock/Field/Synthesis/Generic/Bignum.v
index 4a56bf0bff..3f163b396c 100644
--- a/src/Bedrock/Field/Synthesis/Generic/Bignum.v
+++ b/src/Bedrock/Field/Synthesis/Generic/Bignum.v
@@ -56,7 +56,7 @@ Section Bignum.
           | _ => idtac
           end.
         2:{
-          rewrite firstn_length, Min.min_l by lia.
+          rewrite firstn_length, Nat.min_l by lia.
           destruct Bitwidth.width_cases; subst width; trivial. }
         rewrite chunk_app_chunk; cycle 1.
         { destruct Bitwidth.width_cases; subst width; cbv; inversion 1. }
diff --git a/src/Bedrock/Field/Translation/Proofs/Flatten.v b/src/Bedrock/Field/Translation/Proofs/Flatten.v
index 5294a76d0a..9f441dd311 100644
--- a/src/Bedrock/Field/Translation/Proofs/Flatten.v
+++ b/src/Bedrock/Field/Translation/Proofs/Flatten.v
@@ -1,4 +1,5 @@
 Require Import Coq.Strings.String.
+Require Import Coq.Arith.PeanoNat.
 Require Import Coq.Lists.List.
 Require Import Coq.micromega.Lia.
 Require Import bedrock2.Syntax.
@@ -55,7 +56,7 @@ Section Flatten.
              end.
     erewrite <-IHt1, <-IHt2 by ecancel_assumption.
     rewrite skipn_length, firstn_length.
-    apply Min.min_case_strong; intros; lia.
+    apply Nat.min_case_strong; intros; lia.
   Qed.
 
   (* given these structures have the same type, they'll have the same size in
@@ -80,7 +81,7 @@ Section Flatten.
              end.
     erewrite <-IHt2, <-flatten_base_samelength by ecancel_assumption.
     rewrite skipn_length, firstn_length.
-    apply Min.min_case_strong; intros; lia.
+    apply Nat.min_case_strong; intros; lia.
   Qed.
 
   Lemma of_list_zip_flatten_argnames {t}
@@ -278,6 +279,6 @@ Section Flatten.
              end.
     erewrite <-IHt1, <-IHt2 by ecancel_assumption.
     rewrite skipn_length, firstn_length.
-    apply Min.min_case_strong; intros; lia.
+    apply Nat.min_case_strong; intros; lia.
   Qed.
 End Flatten.
diff --git a/src/Bedrock/Field/Translation/Proofs/UsedVarnames.v b/src/Bedrock/Field/Translation/Proofs/UsedVarnames.v
index e0f1c4831b..08e9439833 100644
--- a/src/Bedrock/Field/Translation/Proofs/UsedVarnames.v
+++ b/src/Bedrock/Field/Translation/Proofs/UsedVarnames.v
@@ -52,7 +52,7 @@ Section UsedVarnames.
              | |- exists _, _ => eexists; solve [eauto with lia]
              end; [ ].
     match goal with H : _ <= _ |- _ =>
-                    apply le_lt_or_eq in H; destruct H; [right | left]
+                    apply Nat.lt_eq_cases in H; destruct H; [right | left]
     end.
     { eexists; eauto with lia. }
     { congruence. }
diff --git a/src/Util/Decidable/Decidable2Bool.v b/src/Util/Decidable/Decidable2Bool.v
index 3c0adbb1f2..f082ad2110 100644
--- a/src/Util/Decidable/Decidable2Bool.v
+++ b/src/Util/Decidable/Decidable2Bool.v
@@ -36,7 +36,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/ListUtil.v b/src/Util/ListUtil.v
index dc9bca368d..3159a193a6 100644
--- a/src/Util/ListUtil.v
+++ b/src/Util/ListUtil.v
@@ -5,7 +5,6 @@ Require Import Coq.Arith.Peano_dec.
 Require Import Coq.ZArith.ZArith.
 Require Import Coq.Arith.Arith.
 Require Import Coq.Classes.Morphisms.
-Require Import Coq.Numbers.Natural.Peano.NPeano.
 Require Import Crypto.Util.NatUtil.
 Require Import Crypto.Util.Pointed.
 Require Import Crypto.Util.Prod.
@@ -211,10 +210,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.
@@ -265,7 +264,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).
@@ -277,7 +276,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.
 
@@ -286,7 +285,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.
@@ -1653,7 +1652,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.
 
@@ -2233,7 +2232,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/WithoutReferenceToZ.v b/src/Util/NUtil/WithoutReferenceToZ.v
index 1955b53d24..89e1f17056 100644
--- a/src/Util/NUtil/WithoutReferenceToZ.v
+++ b/src/Util/NUtil/WithoutReferenceToZ.v
@@ -1,7 +1,6 @@
 (** NUtil that doesn't depend on ZUtil stuff *)
 (** Should probably come up with a better organization of this stuff *)
-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 c7d06d5f46..6e9347cea1 100644
--- a/src/Util/NatUtil.v
+++ b/src/Util/NatUtil.v
@@ -1,7 +1,6 @@
 Require Coq.Logic.Eqdep_dec.
 Require Import Coq.NArith.NArith.
 Require Import Coq.Arith.Arith.
-Require Import Coq.Numbers.Natural.Peano.NPeano.
 Require Import Coq.Classes.Morphisms.
 Require Import Coq.Relations.Relation_Definitions.
 Require Import Coq.micromega.Lia.
@@ -11,7 +10,7 @@ Scheme Equality for nat.
 
 Create HintDb natsimplify discriminated.
 
-Global Hint Resolve mod_bound_pos plus_le_compat : arith.
+Global Hint Resolve mod_bound_pos Nat.add_le_mono : arith.
 #[global]
 Hint Rewrite @mod_small @mod_mod @mod_1_l @mod_1_r succ_pred using lia : natsimplify.
 
@@ -31,9 +30,9 @@ Proof. apply Nat.mod_bound_pos; lia. Qed.
 Global Hint Resolve mod_bound_nonneg mod_bound_lt : arith.
 
 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
@@ -46,8 +45,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.
@@ -175,7 +174,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.
@@ -226,11 +225,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.
@@ -327,7 +326,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 }.
@@ -405,15 +404,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.
diff --git a/src/Util/NumTheoryUtil.v b/src/Util/NumTheoryUtil.v
index 328c0c8236..88bb721812 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.micromega.Lia Coq.Numbers.Natural.Peano.NPeano Coq.Arith.Arith.
+Require Import Coq.micromega.Lia Coq.Arith.Arith.
 Require Import Crypto.Util.ZUtil.Divide.
 Require Import Crypto.Util.ZUtil.Modulo.
 Require Import Crypto.Util.ZUtil.Odd.
diff --git a/src/Util/Strings/String.v b/src/Util/Strings/String.v
index 45ceca5f54..6b9bc469b9 100644
--- a/src/Util/Strings/String.v
+++ b/src/Util/Strings/String.v
@@ -1,4 +1,5 @@
 Require Import Coq.micromega.Lia.
+Require Import Coq.Arith.PeanoNat.
 Require Import Coq.Strings.String.
 Require Import Coq.Strings.Ascii.
 Require Import Crypto.Util.Strings.Ascii.
@@ -130,7 +131,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/Strings/String_as_OT_old.v b/src/Util/Strings/String_as_OT_old.v
index afa4c6e93b..10c32a8ae0 100644
--- a/src/Util/Strings/String_as_OT_old.v
+++ b/src/Util/Strings/String_as_OT_old.v
@@ -117,7 +117,7 @@ Module String_as_OT <: UsualOrderedType.
   Proof.
     intro H; inversion H; subst; auto.
     remember (nat_of_ascii a) as x.
-    apply lt_irrefl in H1; inversion H1.
+    apply Nat.lt_irrefl in H1; inversion H1.
   Qed.
 
   Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
@@ -130,7 +130,7 @@ Module String_as_OT <: UsualOrderedType.
       + constructor. eapply IHx; eauto.
       + constructor; assumption.
       + constructor; assumption.
-      + constructor. eapply lt_trans; eassumption.
+      + constructor. eapply Nat.lt_trans; eassumption.
   Qed.
 
   Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v
index 19280e6e59..925a2be047 100644
--- a/src/Util/Tuple.v
+++ b/src/Util/Tuple.v
@@ -1,4 +1,5 @@
 Require Import Coq.Classes.Morphisms.
+Require Import Coq.Arith.PeanoNat.
 Require Import Coq.Relations.Relation_Definitions.
 Require Import Coq.Lists.List.
 Require Import Coq.micromega.Lia.
@@ -268,7 +269,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 using Type.
diff --git a/src/Util/Wf.v b/src/Util/Wf.v
index 412aba7e46..1eaf894741 100644
--- a/src/Util/Wf.v
+++ b/src/Util/Wf.v
@@ -1,6 +1,7 @@
 (** * Miscellaneous Well-Foundedness Facts *)
 Require Import Coq.Setoids.Setoid Coq.Program.Program Coq.Program.Wf Coq.Arith.Wf_nat Coq.Classes.Morphisms Coq.Init.Wf.
 Require Import Coq.Lists.SetoidList.
+Require Import Coq.Arith.PeanoNat.
 Require Export Crypto.Util.FixCoqMistakes.
 Require Coq.Arith.EqNat.
 
@@ -448,8 +449,8 @@ Section wf.
          | S n' => prod_relationA eqA R (@iterated_prod_relationA n')
          end.
 
-    Fixpoint nat_eq_transfer (P : nat -> Type) (n m : nat) : P n -> (P m) + (EqNat.beq_nat n m = false)
-      := match n, m return P n -> (P m) + (EqNat.beq_nat n m = false) with
+    Fixpoint nat_eq_transfer (P : nat -> Type) (n m : nat) : P n -> (P m) + (Nat.eqb n m = false)
+      := match n, m return P n -> (P m) + (Nat.eqb n m = false) with
          | 0, 0 => fun x => inl x
          | S n', S m' => @nat_eq_transfer (fun v => P (S v)) n' m'
          | _, _ => fun _ => inr eq_refl
@@ -462,11 +463,11 @@ Section wf.
          end.
 
     Fixpoint nat_eq_transfer_neq (P : nat -> Type) (n m : nat)
-      : forall v : P n, (if EqNat.beq_nat n m as b return ((P m) + (b = false)) -> Prop
+      : forall v : P n, (if Nat.eqb n m as b return ((P m) + (b = false)) -> Prop
                          then fun _ => True
                          else fun v => v = inr eq_refl)
                           (nat_eq_transfer P n m v)
-      := match n, m return forall v : P n, (if EqNat.beq_nat n m as b return ((P m) + (b = false)) -> Prop
+      := match n, m return forall v : P n, (if Nat.eqb n m as b return ((P m) + (b = false)) -> Prop
                                             then fun _ => True
                                             else fun v => v = inr eq_refl)
                                              (nat_eq_transfer P n m v)
@@ -522,8 +523,8 @@ Section wf.
                             cbv beta in *;
                             generalize dependent (nat_eq_transfer iterated_prod n1' n0');
                             let Heq := fresh in
-                            destruct (EqNat.beq_nat n1' n0') eqn:Heq;
-                            [ apply EqNat.beq_nat_true_iff in Heq; subst; rewrite <- EqNat.beq_nat_refl in H;
+                            destruct (Nat.eqb n1' n0') eqn:Heq;
+                            [ apply Nat.eqb_eq in Heq; subst; rewrite Nat.eqb_refl in H;
                               exfalso; clear -H; congruence
                             | ]
                        | [ |- context[@nat_eq_transfer iterated_prod n0' n1' _] ]
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index 160a5f8ed3..b3bbbcf3db 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.Numbers.Natural.Peano.NPeano Coq.Arith.Arith.
+Require Coq.micromega.Lia Coq.Arith.Arith.
 Require Crypto.Util.ZUtil.AddGetCarry.
 Require Crypto.Util.ZUtil.AddModulo.
 Require Crypto.Util.ZUtil.CC.
diff --git a/src/Util/ZUtil/Shift.v b/src/Util/ZUtil/Shift.v
index 2644f8cf90..d590aa4103 100644
--- a/src/Util/ZUtil/Shift.v
+++ b/src/Util/ZUtil/Shift.v
@@ -230,13 +230,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).