diff --git a/algebra/cmra.v b/algebra/cmra.v
index 756af9ca3eb6831f42673568d827f9651d382808..177c51ec9f91ba22b84a3484fb0f3f00afe5f0ef 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -791,8 +791,8 @@ Section mnat.
   Instance mnat_valid : Valid mnat := λ x, True.
   Instance mnat_validN : ValidN mnat := λ n x, True.
   Instance mnat_pcore : PCore mnat := Some.
-  Instance mnat_op : Op mnat := max.
-  Definition mnat_op_max x y : x â‹… y = max x y := eq_refl.
+  Instance mnat_op : Op mnat := Nat.max.
+  Definition mnat_op_max x y : x â‹… y = x `max` y := eq_refl.
   Lemma mnat_included (x y : mnat) : x ≼ y ↔ x ≤ y.
   Proof.
     split.
diff --git a/prelude/numbers.v b/prelude/numbers.v
index 2a410297acff4e4e2806531f15bffc6ccf6e0887..0dad1337861dfe92739d36d21f2e48c4549a8aad 100644
--- a/prelude/numbers.v
+++ b/prelude/numbers.v
@@ -32,6 +32,8 @@ Notation "(<)" := lt (only parsing) : nat_scope.
 
 Infix "`div`" := Nat.div (at level 35) : nat_scope.
 Infix "`mod`" := Nat.modulo (at level 35) : nat_scope.
+Infix "`max`" := Nat.max (at level 35) : nat_scope.
+Infix "`min`" := Nat.min (at level 35) : nat_scope.
 
 Instance nat_eq_dec: ∀ x y : nat, Decision (x = y) := eq_nat_dec.
 Instance nat_le_dec: ∀ x y : nat, Decision (x ≤ y) := le_dec.