diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index 9df5355cdbeb3e6c4b00ef2fa4a87edc34bf9fe7..7059e8b611b07ae64456d268df9b4162b19a2c60 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -1116,6 +1116,8 @@ Section prod.
 
   Lemma pair_op (a a' : A) (b b' : B) : (a, b) â‹… (a', b') = (a â‹… a', b â‹… b').
   Proof. done. Qed.
+  Lemma pair_valid (a : A) (b : B) : ✓ (a, b) ↔ ✓ a ∧ ✓ b.
+  Proof. done. Qed.
 
   Global Instance prod_cmra_total : CmraTotal A → CmraTotal B → CmraTotal prodR.
   Proof.