diff --git a/algebra/cmra.v b/algebra/cmra.v
index 689433b1925d783da5f5386726015598a2c88478..c0c4dc515697643e3eb663ee94f24fac94197e9d 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -984,6 +984,10 @@ Section prod_unit.
 
   Lemma pair_split (x : A) (y : B) : (x, y) ≡ (x, ∅) ⋅ (∅, y).
   Proof. by rewrite pair_op left_id right_id. Qed.
+
+  Lemma pair_split_L `{!LeibnizEquiv A, !LeibnizEquiv B} (x : A) (y : B) :
+    (x, y) = (x, ∅) ⋅ (∅, y).
+  Proof. unfold_leibniz. apply pair_split. Qed.
 End prod_unit.
 
 Arguments prodUR : clear implicits.