diff --git a/tests/notation.v b/tests/notation.v
index 41fe94e9cea8db3335688669f0386d3c196390a7..b1b3df82c80ce8f08a768e8be791365b1f6e7106 100644
--- a/tests/notation.v
+++ b/tests/notation.v
@@ -18,7 +18,7 @@ Section map_notations.
   Definition test_4 : M (M nat) := {[ 10 := {[ 10 := 1 ]}; 20 := {[ 20 := 2]};
     30 := {[ 30 := 3]}; 40 := {[ 40 := 4 ]} ]}.
 
-  Definition test_op_2 : M (M nat) := {[ 10 := {[pow 10 2 := 99]};
+  Definition test_op_2 : M (M nat) := {[ 10 := {[Nat.pow 10 2 := 99]};
     10 + 1 := {[ 10 - 100 := 42 * 1337 ]} ]}.
 
   Definition test_op_3 : M (M (list nat)) := {[ 10 := {[ 20 - 2 := [11]; 1 := [22] ]};
@@ -48,4 +48,4 @@ Section multiset_notations.
   Print test_gmultiset_2.
   Print test_gmultiset_3.
   Print test_gmultiset_4.
-End multiset_notations.
\ No newline at end of file
+End multiset_notations.
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index b5d8197dc23d328e13ee23bf42ba3f508320a6b9..6cb16d4ea5bf867750440e3962959d8bb18c7164 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -1156,7 +1156,7 @@ Lemma map_to_list_length {A} (m1 m2 : M A) :
 Proof.
   revert m2. induction m1 as [|i x m ? IH] using map_ind.
   { intros m2 Hm2. rewrite map_to_list_empty. simpl.
-    apply neq_0_lt. intros Hlen. symmetry in Hlen.
+    apply Nat.neq_0_lt_0, Nat.neq_sym. intros Hlen. symmetry in Hlen.
     apply nil_length_inv, map_to_list_empty_iff in Hlen.
     rewrite Hlen in Hm2. destruct (irreflexivity (⊂) ∅ Hm2). }
   intros m2 Hm2.
diff --git a/theories/list.v b/theories/list.v
index a884e8d2d732090937ee93484dea44e8f6b55569..ef0d56691bfaaedc05ea59a8b80f12b2dfc4947b 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -1204,13 +1204,13 @@ Proof. revert n. induction l; intros [|?] ?; f_equal/=; auto with lia. Qed.
 Lemma take_take l n m : take n (take m l) = take (min n m) l.
 Proof. revert n m. induction l; intros [|?] [|?]; f_equal/=; auto. Qed.
 Lemma take_idemp l n : take n (take n l) = take n l.
-Proof. by rewrite take_take, Min.min_idempotent. Qed.
+Proof. by rewrite take_take, Nat.min_id. Qed.
 Lemma take_length l n : length (take n l) = min n (length l).
 Proof. revert n. induction l; intros [|?]; f_equal/=; done. Qed.
 Lemma take_length_le l n : n ≤ length l → length (take n l) = n.
-Proof. rewrite take_length. apply Min.min_l. Qed.
+Proof. rewrite take_length. apply Nat.min_l. Qed.
 Lemma take_length_ge l n : length l ≤ n → length (take n l) = length l.
-Proof. rewrite take_length. apply Min.min_r. Qed.
+Proof. rewrite take_length. apply Nat.min_r. Qed.
 Lemma take_drop_commute l n m : take n (drop m l) = drop m (take (m + n) l).
 Proof.
   revert n m. induction l; intros [|?][|?]; simpl; auto using take_nil with lia.
@@ -1483,9 +1483,9 @@ Proof.
   revert n m. induction l; intros [|?][|?]; f_equal/=; auto using take_replicate.
 Qed.
 Lemma take_resize_le l n m x : n ≤ m → take n (resize m x l) = resize n x l.
-Proof. intros. by rewrite take_resize, Min.min_l. Qed.
+Proof. intros. by rewrite take_resize, Nat.min_l. Qed.
 Lemma take_resize_eq l n x : take n (resize n x l) = resize n x l.
-Proof. intros. by rewrite take_resize, Min.min_l. Qed.
+Proof. intros. by rewrite take_resize, Nat.min_l. Qed.
 Lemma take_resize_plus l n m x : take n (resize (n + m) x l) = resize n x l.
 Proof. by rewrite take_resize, min_l by lia. Qed.
 Lemma drop_resize_le l n m x :
@@ -1699,7 +1699,7 @@ Proof.
     repeat match goal with
     | H : _ ≤ length _ |- _ => rewrite take_length, drop_length in H
     end; rewrite ?take_drop_commute, ?drop_drop, ?take_take,
-      ?Min.min_l, Nat.add_assoc by lia; auto with lia.
+      ?Nat.min_l, Nat.add_assoc by lia; auto with lia.
 Qed.
 Lemma sublist_alter_length f l i n k :
   sublist_lookup i n l = Some k → length (f k) = n →
@@ -3256,7 +3256,7 @@ Section Forall2.
     { rewrite <-(resize_resize l m n) by done. by apply Forall2_resize. }
     intros. assert (n = length k); subst.
     { by rewrite <-(Forall2_length (resize n x l) k), resize_length. }
-    rewrite (le_plus_minus (length k) m), !resize_plus,
+    rewrite (nat_le_plus_minus (length k) m), !resize_plus,
       resize_all, drop_all, resize_nil by lia.
     auto using Forall2_app, Forall2_replicate_r,
       Forall_resize, Forall_drop, resize_length.
@@ -3269,7 +3269,7 @@ Section Forall2.
     { rewrite <-(resize_resize k m n) by done. by apply Forall2_resize. }
     assert (n = length l); subst.
     { by rewrite (Forall2_length l (resize n y k)), resize_length. }
-    rewrite (le_plus_minus (length l) m), !resize_plus,
+    rewrite (nat_le_plus_minus (length l) m), !resize_plus,
       resize_all, drop_all, resize_nil by lia.
     auto using Forall2_app, Forall2_replicate_l,
       Forall_resize, Forall_drop, resize_length.
@@ -3318,7 +3318,7 @@ Section Forall2.
     apply Forall2_app_l;
       rewrite ?take_length_le by lia; auto using Forall2_take.
     apply Forall2_app_l; erewrite Forall2_length, take_length,
-      drop_length, <-Forall2_length, Min.min_l by eauto with lia; [done|].
+      drop_length, <-Forall2_length, Nat.min_l by eauto with lia; [done|].
     rewrite drop_drop; auto using Forall2_drop.
   Qed.
 
@@ -3652,7 +3652,7 @@ Section find.
           naive_solver eauto using lookup_app_l_Some with lia. }
         apply list_find_Some. split_and!; [done..|].
         intros j z ??. eapply (Hleast (length l1 + j)); [|lia].
-        by rewrite lookup_app_r, minus_plus by lia.
+        by rewrite lookup_app_r, nat_minus_plus by lia.
     - intros [(?&?&Hleast)%list_find_Some|(?&Hl1&(?&?&Hleast)%list_find_Some)].
       + apply list_find_Some. split_and!; [by auto using lookup_app_l_Some..|].
         assert (i < length l1) by eauto using lookup_lt_Some.
diff --git a/theories/numbers.v b/theories/numbers.v
index 4acc4adf9dc0a68ba9a8e1de202a109041294494..4f72314302e0bfea69cae39fd9fda484d4e258cc 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -65,6 +65,13 @@ Proof. unfold lt. apply _. Qed.
 Lemma nat_le_sum (x y : nat) : x ≤ y ↔ ∃ z, y = x + z.
 Proof. split; [exists (y - x); lia | intros [z ->]; lia]. Qed.
 
+(** [Arith.Minus.minus_plus] is deprecated starting in 8.16 *)
+Lemma nat_minus_plus n m : n + m - n = m.
+Proof. lia. Qed.
+(** [Arith.Minus.le_plus_minus] is deprecated starting in 8.16 *)
+Lemma nat_le_plus_minus n m : n ≤ m → m = n + (m - n).
+Proof. lia. Qed.
+
 Lemma Nat_lt_succ_succ n : n < S (S n).
 Proof. auto with arith. Qed.
 Lemma Nat_mul_split_l n x1 x2 y1 y2 :
@@ -1371,7 +1378,7 @@ Lemma rotate_nat_add_add base offset len n:
 Proof.
   intros ?. unfold rotate_nat_add.
   rewrite !Z2Nat_inj_mod, !Z2Nat.inj_add, !Nat2Z.id by lia.
-  by rewrite plus_assoc, Nat.add_mod_idemp_l by lia.
+  by rewrite Nat.add_assoc, Nat.add_mod_idemp_l by lia.
 Qed.
 
 Lemma rotate_nat_add_S base offset len:
diff --git a/theories/relations.v b/theories/relations.v
index 3403317828aa1170e807642e277179f733e04028..c09ae6b9c940961879d4f7a7cee513d3cb9a7a82 100644
--- a/theories/relations.v
+++ b/theories/relations.v
@@ -177,7 +177,7 @@ Section general.
   Lemma bsteps_weaken n m x y :
     n ≤ m → bsteps R n x y → bsteps R m x y.
   Proof.
-    intros. rewrite (Minus.le_plus_minus n m); auto using bsteps_plus_r.
+    intros. rewrite (nat_le_plus_minus n m); auto using bsteps_plus_r.
   Qed.
   Lemma bsteps_plus_l n m x y :
     bsteps R n x y → bsteps R (m + n) x y.