From f70dd438615606c3cfe216b72b69409084524e8e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 3 Jul 2016 16:02:08 +0200
Subject: [PATCH] Mononicity of auth_own.

---
 program_logic/auth.v | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/program_logic/auth.v b/program_logic/auth.v
index 6f966d983..58d63dcd9 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -55,6 +55,10 @@ Section auth.
 
   Lemma auth_own_op γ a b : auth_own γ (a ⋅ b) ⊣⊢ auth_own γ a ★ auth_own γ b.
   Proof. by rewrite /auth_own -own_op auth_frag_op. Qed.
+
+  Lemma auth_own_mono γ a b : a ≼ b → auth_own γ b ⊢ auth_own γ a.
+  Proof. intros [? ->]. by rewrite auth_own_op sep_elim_l. Qed.
+
   Lemma auth_own_valid γ a : auth_own γ a ⊢ ✓ a.
   Proof. by rewrite /auth_own own_valid auth_validI. Qed.
 
-- 
GitLab