From dad8a9a72e75295316eaa62fbd47903243eafb52 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 23 May 2016 00:55:42 +0200
Subject: [PATCH] Misc property about the product CMRA.

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

diff --git a/algebra/cmra.v b/algebra/cmra.v
index 7a25c150f..fadeb8576 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -580,6 +580,10 @@ Section prod.
     Persistent x → Persistent y → Persistent (x,y).
   Proof. by split. Qed.
 
+  Lemma pair_split `{CMRAUnit A, CMRAUnit B} (x : A) (y : B) :
+    (x, y) ≡ (x, ∅) ⋅ (∅, y).
+  Proof. constructor; by rewrite /= ?left_id ?right_id. Qed.
+
   Lemma prod_update x y : x.1 ~~> y.1 → x.2 ~~> y.2 → x ~~> y.
   Proof. intros ?? n z [??]; split; simpl in *; auto. Qed.
   Lemma prod_updateP P1 P2 (Q : A * B → Prop)  x :
-- 
GitLab