diff --git a/iris/algebra/csum.v b/iris/algebra/csum.v
index 8ff770410eafaf95e2e40053044c3e8ff36a91c8..95fe7172d7dcd5b89ded63c003db4c746a0003ae 100644
--- a/iris/algebra/csum.v
+++ b/iris/algebra/csum.v
@@ -178,6 +178,11 @@ Proof. done. Qed.
 Lemma Cinr_op b b' : Cinr (b â‹… b') = Cinr b â‹… Cinr b'.
 Proof. done. Qed.
 
+Lemma Cinl_valid a : ✓ (Cinl a) ↔ ✓ a.
+Proof. done. Qed.
+Lemma Cinr_valid b : ✓ (Cinr b) ↔ ✓ b.
+Proof. done. Qed.
+
 Lemma csum_included x y :
   x ≼ y ↔ y = CsumBot ∨ (∃ a a', x = Cinl a ∧ y = Cinl a' ∧ a ≼ a')
                       ∨ (∃ b b', x = Cinr b ∧ y = Cinr b' ∧ b ≼ b').