diff --git a/iris/algebra/lib/frac_auth.v b/iris/algebra/lib/frac_auth.v
index 882d480fb2f8d0a7eb7c7fa0057c7ab8da189796..4ea484de6a034860b08f3ae07ba3feca4f009143 100644
--- a/iris/algebra/lib/frac_auth.v
+++ b/iris/algebra/lib/frac_auth.v
@@ -92,16 +92,12 @@ Section frac_auth.
   Lemma frac_auth_frag_op q1 q2 a1 a2 : ◯F{q1+q2} (a1 ⋅ a2) ≡ ◯F{q1} a1 ⋅ ◯F{q2} a2.
   Proof. done. Qed.
 
-  Lemma frac_auth_frag_validN_op_1_l n q a b : ✓{n} (◯F{1} a ⋅ ◯F{q} b) ↔ False.
-  Proof.
-    rewrite -frac_auth_frag_op frac_auth_frag_validN.
-    pose proof (Qp_not_add_le_l 1 q); tauto.
-  Qed.
-  Lemma frac_auth_frag_valid_op_1_l q a b : ✓ (◯F{1} a ⋅ ◯F{q} b) ↔ False.
-  Proof.
-    rewrite -frac_auth_frag_op frac_auth_frag_valid.
-    pose proof (Qp_not_add_le_l 1 q); tauto.
-  Qed.
+  Lemma frac_auth_frag_op_validN n q1 q2 a b :
+    ✓{n} (◯F{q1} a ⋅ ◯F{q2} b) ↔ (q1 + q2 ≤ 1)%Qp ∧ ✓{n} (a ⋅ b).
+  Proof. by rewrite -frac_auth_frag_op frac_auth_frag_validN. Qed.
+  Lemma frac_auth_frag_op_valid q1 q2 a b :
+    ✓ (◯F{q1} a ⋅ ◯F{q2} b) ↔ (q1 + q2 ≤ 1)%Qp ∧ ✓ (a ⋅ b).
+  Proof. by rewrite -frac_auth_frag_op frac_auth_frag_valid. Qed.
 
   Global Instance frac_auth_is_op (q q1 q2 : frac) (a a1 a2 : A) :
     IsOp q q1 q2 → IsOp a a1 a2 → IsOp' (◯F{q} a) (◯F{q1} a1) (◯F{q2} a2).
diff --git a/iris/algebra/lib/ufrac_auth.v b/iris/algebra/lib/ufrac_auth.v
index d577614c7d5312097cfb22edeef643551556c338..6617975b92f1e1f5a705943746ca5c1650bacab3 100644
--- a/iris/algebra/lib/ufrac_auth.v
+++ b/iris/algebra/lib/ufrac_auth.v
@@ -13,8 +13,8 @@ difference:
 ✓ (a ⋅ b) → ●U_p a ~~> ●U_(p + q) (a ⋅ b) ⋅ ◯U_q b
 >>
 
-- We no longer have the [â—¯U{1} a] is the exclusive fragmental element (cf.
-  [frac_auth_frag_validN_op_1_l]).
+- We no longer have the [â—¯U_1 a] is an exclusive fragmental element. That is,
+  while [â—¯F{1} a â‹… â—¯F{q} b] is vacuously false, [â—¯U_1 a â‹… â—¯U_q2 b] is not.
 *)
 From iris.algebra Require Export auth frac updates local_updates.
 From iris.algebra Require Import ufrac proofmode_classes.