From 2bc63edbf375ca9a476237ce0c80c361ccf49eee Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 18 Jul 2022 14:54:32 +0200
Subject: [PATCH] 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 | 14 ++++++++++----
 1 file changed, 10 insertions(+), 4 deletions(-)

diff --git a/iris/algebra/lib/frac_auth.v b/iris/algebra/lib/frac_auth.v
index 412ada8e4..882d480fb 100644
--- a/iris/algebra/lib/frac_auth.v
+++ b/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).
-- 
GitLab