From 7298dd395f8a8953434ed547c84b2848ad33cdec Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 29 Nov 2017 22:59:59 +0100
Subject: [PATCH] =?UTF-8?q?Prove=20`x=20=E2=8B=85=20y=20~~>=20x`.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/algebra/updates.v | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/theories/algebra/updates.v b/theories/algebra/updates.v
index 169b78a66..372130355 100644
--- a/theories/algebra/updates.v
+++ b/theories/algebra/updates.v
@@ -77,6 +77,12 @@ Lemma cmra_update_op x1 x2 y1 y2 : x1 ~~> y1 → x2 ~~> y2 → x1 ⋅ x2 ~~> y1
 Proof.
   rewrite !cmra_update_updateP; eauto using cmra_updateP_op with congruence.
 Qed.
+
+Lemma cmra_update_op_l x y : x â‹… y ~~> x.
+Proof. intros n mz. rewrite comm cmra_opM_assoc. apply cmra_validN_op_r. Qed.
+Lemma cmra_update_op_r x y : x â‹… y ~~> y.
+Proof. rewrite comm. apply cmra_update_op_l. Qed.
+
 Lemma cmra_update_valid0 x y : (✓{0} x → x ~~> y) → x ~~> y.
 Proof.
   intros H n mz Hmz. apply H, Hmz.
-- 
GitLab