diff --git a/iris/algebra/lib/mono_nat.v b/iris/algebra/lib/mono_nat.v
index 461382f81a6ae690efdf68b1ad56efe2ae1f77c5..b712ad6e87424d14e6b76cc6dc28d553b9360378 100644
--- a/iris/algebra/lib/mono_nat.v
+++ b/iris/algebra/lib/mono_nat.v
@@ -40,9 +40,6 @@ Section mono_nat.
     rewrite (comm _ (●{dq2} _)) -!assoc (assoc _ (◯ _)).
     by rewrite -core_id_dup (comm _ (â—¯ _)).
   Qed.
-  Lemma mono_nat_auth_frac_op q1 q2 n :
-    ●MN{#(q1 + q2)} n ≡ ●MN{#q1} n ⋅ ●MN{#q2} n.
-  Proof. by rewrite -mono_nat_auth_dfrac_op dfrac_op_own. Qed.
 
   Lemma mono_nat_lb_op n1 n2 :
     â—¯MN (n1 `max` n2) = â—¯MN n1 â‹… â—¯MN n2.
@@ -79,9 +76,6 @@ Section mono_nat.
     - intros [? ->]. rewrite -core_id_dup -auth_auth_dfrac_op.
       by apply auth_both_dfrac_valid_discrete.
   Qed.
-  Lemma mono_nat_auth_frac_op_valid q1 q2 n1 n2 :
-    ✓ (●MN{#q1} n1 ⋅ ●MN{#q2} n2) ↔ (q1 + q2 ≤ 1)%Qp ∧ n1 = n2.
-  Proof. by apply mono_nat_auth_dfrac_op_valid. Qed.
   Lemma mono_nat_auth_op_valid n1 n2 :
     ✓ (●MN n1 ⋅ ●MN n2) ↔ False.
   Proof. rewrite mono_nat_auth_dfrac_op_valid. naive_solver. Qed.
diff --git a/iris/base_logic/lib/mono_nat.v b/iris/base_logic/lib/mono_nat.v
index 3118b0956e202145c1bf099e0d9236959321935c..99389ea1d11c82650061c9a2e39cca5eae6eb45b 100644
--- a/iris/base_logic/lib/mono_nat.v
+++ b/iris/base_logic/lib/mono_nat.v
@@ -53,7 +53,7 @@ Section mono_nat.
 
   Global Instance mono_nat_auth_own_fractional γ n :
     Fractional (λ q, mono_nat_auth_own γ q n).
-  Proof. unseal. intros p q. rewrite -own_op mono_nat_auth_frac_op //. Qed.
+  Proof. unseal. intros p q. rewrite -own_op -mono_nat_auth_dfrac_op //. Qed.
   Global Instance mono_nat_auth_own_as_fractional γ q n :
     AsFractional (mono_nat_auth_own γ q n) (λ q, mono_nat_auth_own γ q n) q.
   Proof. split; [auto|apply _]. Qed.