From 921b37b8c019738afd3bbb646b2c9402388f00ec Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 12 Sep 2020 13:12:22 +0200
Subject: [PATCH] Misc trivial camera lemmas.

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

diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index 668c23f5a..bda4fdbc1 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -1165,10 +1165,14 @@ Section prod.
   Proof. done. Qed.
   Lemma pair_valid (a : A) (b : B) : ✓ (a, b) ↔ ✓ a ∧ ✓ b.
   Proof. done. Qed.
+  Lemma pair_validN n (a : A) (b : B) : ✓{n} (a, b) ↔ ✓{n} a ∧ ✓{n} b.
+  Proof. done. Qed.
   Lemma pair_included (a a' : A) (b b' : B) :
     (a, b) ≼ (a', b') ↔ a ≼ a' ∧ b ≼ b'.
   Proof. apply prod_included. Qed.
-
+  Lemma pair_pcore (a : A) (b : B) :
+    pcore (a, b) = c1 ← pcore a; c2 ← pcore b; Some (c1, c2).
+  Proof. done. Qed.
   Lemma pair_core `{!CmraTotal A, !CmraTotal B} (a : A) (b : B) :
     core (a, b) = (core a, core b).
   Proof.
-- 
GitLab