From fdec4152db225cd2d59842723f35739990a89db4 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 11 Feb 2016 20:04:46 +0100
Subject: [PATCH] Missing cmra_preserving lemmas.

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

diff --git a/algebra/cmra.v b/algebra/cmra.v
index 807139069..943de0cd2 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -272,8 +272,12 @@ Lemma cmra_unit_preserving x y : x ≼ y → unit x ≼ unit y.
 Proof. rewrite !cmra_included_includedN; eauto using cmra_unit_preservingN. Qed.
 Lemma cmra_included_unit x : unit x ≼ x.
 Proof. by exists x; rewrite cmra_unit_l. Qed.
+Lemma cmra_preservingN_l n x y z : x ≼{n} y → z ⋅ x ≼{n} z ⋅ y.
+Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1 (associative op). Qed.
 Lemma cmra_preserving_l x y z : x ≼ y → z ⋅ x ≼ z ⋅ y.
 Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1 (associative op). Qed.
+Lemma cmra_preservingN_r n x y z : x ≼{n} y → x ⋅ z ≼{n} y ⋅ z.
+Proof. by intros; rewrite -!(commutative _ z); apply cmra_preservingN_l. Qed.
 Lemma cmra_preserving_r x y z : x ≼ y → x ⋅ z ≼ y ⋅ z.
 Proof. by intros; rewrite -!(commutative _ z); apply cmra_preserving_l. Qed.
 
-- 
GitLab