diff --git a/iris/algebra/dfrac.v b/iris/algebra/dfrac.v
index f38afd0e4f0eb0c2c05cb4755ba6add697fcd2f1..30969cbbaffb53703eeb818f854bd1c07a9e3659 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 06115f125d98c8b437d39a100ef564f5b5affef3..0747d5a1e7a51d48afcf2d5795818f15c9f915f5 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.