diff --git a/theories/numbers.v b/theories/numbers.v
index 2455887c1c02e0402ea44116333025b7560829a3..80dc45a1f6e6b0fa5285022cddf39ca74f391cd0 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -15,6 +15,8 @@ Proof. solve_decision. Defined.
 
 (** * Notations and properties of [nat] *)
 Arguments minus !_ !_ / : assert.
+Arguments Nat.max : simpl nomatch.
+
 Reserved Notation "x ≤ y ≤ z" (at level 70, y at next level).
 Reserved Notation "x ≤ y < z" (at level 70, y at next level).
 Reserved Notation "x < y < z" (at level 70, y at next level).