From 8e5241da6b93a619b0de9c0d9b249f1ffc23d5f0 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 19 Jul 2022 11:18:34 -0400
Subject: [PATCH] add lemams for validity of the 1 fraction

---
 iris/algebra/dfrac.v | 2 ++
 iris/algebra/frac.v  | 2 ++
 2 files changed, 4 insertions(+)

diff --git a/iris/algebra/dfrac.v b/iris/algebra/dfrac.v
index f38afd0e4..30969cbba 100644
--- a/iris/algebra/dfrac.v
+++ b/iris/algebra/dfrac.v
@@ -160,6 +160,8 @@ Section dfrac.
 
   Lemma dfrac_valid_own p : ✓ DfracOwn p ↔ (p ≤ 1)%Qp.
   Proof. done. Qed.
+  Lemma dfrac_valid_own_1 : ✓ DfracOwn 1.
+  Proof. done. Qed.
 
   Lemma dfrac_valid_own_r dq q : ✓ (dq ⋅ DfracOwn q) → (q < 1)%Qp.
   Proof.
diff --git a/iris/algebra/frac.v b/iris/algebra/frac.v
index 06115f125..0747d5a1e 100644
--- a/iris/algebra/frac.v
+++ b/iris/algebra/frac.v
@@ -21,6 +21,8 @@ Section frac.
 
   Lemma frac_valid p : ✓ p ↔ (p ≤ 1)%Qp.
   Proof. done. Qed.
+  Lemma frac_valid_1 : ✓ 1%Qp.
+  Proof. done. Qed.
   Lemma frac_op p q : p â‹… q = (p + q)%Qp.
   Proof. done. Qed.
   Lemma frac_included p q : p ≼ q ↔ (p < q)%Qp.
-- 
GitLab