diff --git a/theories/numbers.v b/theories/numbers.v
index df8c21a25c6b051cfb23e0d03af4a87ecad61e80..72ca465cd587fcc1bfe09d801112469d55013360 100644
--- a/theories/numbers.v
+++ b/theories/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.