diff --git a/iris/algebra/lib/mono_nat.v b/iris/algebra/lib/mono_nat.v
index 7f63321098e7fef40064a42c1dcf41e3b9a3843b..4d95547a9d5bca63e1ab3de3536fb6e379ce07d6 100644
--- a/iris/algebra/lib/mono_nat.v
+++ b/iris/algebra/lib/mono_nat.v
@@ -79,7 +79,7 @@ Section mono_nat.
   Lemma mono_nat_included q n : mono_nat_lb n ≼ mono_nat_auth q n.
   Proof. apply cmra_included_r. Qed.
 
-  Lemma mono_nat_update n n' :
+  Lemma mono_nat_update {n} n' :
     n ≤ n' →
     mono_nat_auth 1 n ~~> mono_nat_auth 1 n'.
   Proof.