Remove unidirectional lemmas with `1` fraction `frac_auth_frag_validN_op_1_l`

and `frac_auth_frag_valid_op_1_l`, add `frac_auth_frag_op_validN` and
`frac_auth_frag_op_valid`, which are bi-implications with arbitrary fractions.

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).

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.