From c6e56bd3df9c7d56fecb2f6473c8edf4cfa45d6f Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 15 Jul 2022 15:08:48 -0400
Subject: [PATCH] add mono_nat_lb_own_0

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

diff --git a/iris/base_logic/lib/mono_nat.v b/iris/base_logic/lib/mono_nat.v
index f093b3baf..02df5fafe 100644
--- a/iris/base_logic/lib/mono_nat.v
+++ b/iris/base_logic/lib/mono_nat.v
@@ -97,6 +97,10 @@ Section mono_nat.
     mono_nat_lb_own γ n -∗ mono_nat_lb_own γ n'.
   Proof. unseal. intros. by apply own_mono, mono_nat_lb_mono. Qed.
 
+  Lemma mono_nat_lb_own_0 γ :
+    ⊢ |==> mono_nat_lb_own γ 0.
+  Proof. unseal. iApply own_unit. Qed.
+
   Lemma mono_nat_own_alloc n :
     ⊢ |==> ∃ γ, mono_nat_auth_own γ 1 n ∗ mono_nat_lb_own γ n.
   Proof.
-- 
GitLab