Turn `frac_auth_frag_validN_op_1_l` and `frac_auth_frag_valid_op_1_l` into bi-implications.

iris/algebra/lib/frac_auth.v

@@ -92,10 +92,16 @@ 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=> -[/Qp_not_add_le_l []]. 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=> -[/Qp_not_add_le_l []]. 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.
 
   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).