From d44228a5ebf9c41ad21f368391fddb9ed1903e80 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 14 Feb 2016 21:58:04 +0100
Subject: [PATCH] Left and right mononicity properties for uPred_sep.

---
 algebra/upred.v | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/algebra/upred.v b/algebra/upred.v
index d0a4d6f67..848ba2ad5 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -576,6 +576,10 @@ Proof. by intros x n ? (x1&x2&Hx&HPQ&?); cofe_subst; apply HPQ. Qed.
 
 (* Derived BI Stuff *)
 Hint Resolve sep_mono.
+Lemma sep_mono_l P P' Q : P ⊑ Q → (P ★ P') ⊑ (Q ★ P').
+Proof. by intros; apply sep_mono. Qed.
+Lemma sep_mono_r P P' Q' : P' ⊑ Q' → (P ★ P') ⊑ (P ★ Q').
+Proof. by apply sep_mono. Qed.
 Global Instance sep_mono' : Proper ((⊑) ==> (⊑) ==> (⊑)) (@uPred_sep M).
 Proof. by intros P P' HP Q Q' HQ; apply sep_mono. Qed.
 Global Instance sep_flip_mono' :
-- 
GitLab