diff --git a/iris/algebra/numbers.v b/iris/algebra/numbers.v
index a04152916f67764e7d373e940da968ba0a14b1dd..349be4dfd622c941d4f5e0fbcbd64a3af77ef059 100644
--- a/iris/algebra/numbers.v
+++ b/iris/algebra/numbers.v
@@ -69,7 +69,7 @@ Section max_nat.
     apply ra_total_mixin; apply _ || eauto.
     - intros [x] [y] [z]. repeat rewrite max_nat_op. by rewrite Nat.max_assoc.
     - intros [x] [y]. by rewrite max_nat_op Nat.max_comm.
-    - intros [x]. by rewrite max_nat_op Max.max_idempotent.
+    - intros [x]. by rewrite max_nat_op Nat.max_id.
   Qed.
   Canonical Structure max_natR : cmra := discreteR max_nat max_nat_ra_mixin.
 
@@ -124,7 +124,7 @@ Section min_nat.
     apply ra_total_mixin; apply _ || eauto.
     - intros [x] [y] [z]. repeat rewrite min_nat_op_min. by rewrite Nat.min_assoc.
     - intros [x] [y]. by rewrite min_nat_op_min Nat.min_comm.
-    - intros [x]. by rewrite min_nat_op_min Min.min_idempotent.
+    - intros [x]. by rewrite min_nat_op_min Nat.min_id.
   Qed.
   Canonical Structure min_natR : cmra := discreteR min_nat min_nat_ra_mixin.
 
@@ -147,7 +147,7 @@ Section min_nat.
   Proof. done. Qed.
 
   Global Instance : RightAbsorb (=) (MinNat 0) (â‹…).
-  Proof. intros [x]. by rewrite min_nat_op_min Min.min_0_r. Qed.
+  Proof. intros [x]. by rewrite min_nat_op_min Nat.min_0_r. Qed.
 
   Global Instance : IdemP (=@{min_nat}) (â‹…).
   Proof. intros [x]. rewrite min_nat_op_min. apply f_equal. lia. Qed.