diff --git a/iris/algebra/lib/mono_nat.v b/iris/algebra/lib/mono_nat.v
index defd93831881f6991888911f501abc6c03853c52..461382f81a6ae690efdf68b1ad56efe2ae1f77c5 100644
--- a/iris/algebra/lib/mono_nat.v
+++ b/iris/algebra/lib/mono_nat.v
@@ -45,7 +45,7 @@ Section mono_nat.
   Proof. by rewrite -mono_nat_auth_dfrac_op dfrac_op_own. Qed.
 
   Lemma mono_nat_lb_op n1 n2 :
-    â—¯MN n1 â‹… â—¯MN n2 = â—¯MN (n1 `max` n2).
+    â—¯MN (n1 `max` n2) = â—¯MN n1 â‹… â—¯MN n2.
   Proof. rewrite -auth_frag_op max_nat_op //. Qed.
 
   Lemma mono_nat_auth_lb_op dq n :
@@ -61,7 +61,7 @@ Section mono_nat.
   Lemma mono_nat_lb_op_le_l n n' :
     n' ≤ n →
     â—¯MN n = â—¯MN n' â‹… â—¯MN n.
-  Proof. intros. rewrite mono_nat_lb_op Nat.max_r //. Qed.
+  Proof. intros. rewrite -mono_nat_lb_op Nat.max_r //. Qed.
 
   Lemma mono_nat_auth_dfrac_valid dq n : (✓ ●MN{dq} n) ↔ ✓ dq.
   Proof.