diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index 3ea70b65a0f24fd8b5f715016cad68a014b8e460..8a409fdbf3dc60d02883fc51905a21855ea681fb 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -1210,6 +1210,20 @@ Section prod_unit.
   Lemma pair_split_L `{!LeibnizEquiv A, !LeibnizEquiv B} (x : A) (y : B) :
     (x, y) = (x, ε) ⋅ (ε, y).
   Proof. unfold_leibniz. apply pair_split. Qed.
+
+  Lemma pair_op_1 (a a': A) : (a ⋅ a', ε) ≡@{A*B} (a, ε) ⋅ (a', ε).
+  Proof. by rewrite -pair_op ucmra_unit_left_id. Qed.
+
+  Lemma pair_op_1_L `{!LeibnizEquiv A, !LeibnizEquiv B} (a a': A) :
+    (a ⋅ a', ε) =@{A*B} (a, ε) ⋅ (a', ε).
+  Proof. unfold_leibniz. apply pair_op_1. Qed.
+
+  Lemma pair_op_2 (b b': B) : (ε, b ⋅ b') ≡@{A*B} (ε, b) ⋅ (ε, b').
+  Proof. by rewrite -pair_op ucmra_unit_left_id. Qed.
+
+  Lemma pair_op_2_L `{!LeibnizEquiv A, !LeibnizEquiv B} (b b': B) :
+    (ε, b ⋅ b') =@{A*B} (ε, b) ⋅ (ε, b').
+  Proof. unfold_leibniz. apply pair_op_2. Qed.
 End prod_unit.
 
 Arguments prodUR : clear implicits.