From 3423128f085980271a052800c41e5db8d690e008 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 18 Dec 2020 17:53:52 +0100
Subject: [PATCH] add mono_nat_auth_lb

---
 iris/algebra/lib/mono_nat.v | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/iris/algebra/lib/mono_nat.v b/iris/algebra/lib/mono_nat.v
index 4d95547a9..9079edf39 100644
--- a/iris/algebra/lib/mono_nat.v
+++ b/iris/algebra/lib/mono_nat.v
@@ -35,6 +35,14 @@ Section mono_nat.
     mono_nat_lb n1 â‹… mono_nat_lb n2 = mono_nat_lb (n1 `max` n2).
   Proof. rewrite -auth_frag_op max_nat_op_max //. Qed.
 
+  Lemma mono_nat_auth_lb_op q n :
+    mono_nat_auth q n ≡ mono_nat_auth q n ⋅ mono_nat_lb n.
+  Proof.
+    rewrite /mono_nat_auth /mono_nat_lb.
+    rewrite -!assoc -auth_frag_op max_nat_op_max.
+    rewrite Nat.max_id //.
+  Qed.
+
   (** rephrasing of [mono_nat_lb_op] useful for weakening a fragment to a
   smaller lower-bound *)
   Lemma mono_nat_lb_op_le_l n n' :
-- 
GitLab