diff --git a/algebra/cmra.v b/algebra/cmra.v
index abe9a0b2b7568575d008fdb21b135218eb398229..e01c27716452285a0ff22ec31210cda3a8275a50 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -985,8 +985,7 @@ Section prod.
   Canonical Structure prodR :=
     CMRAT (A * B) prod_cofe_mixin prod_cmra_mixin.
 
-  Lemma pair_op (a a' : A) (b b' : B) :
-    (a, b) ⋅ (a', b') ≡ (a ⋅ a', b ⋅ b').
+  Lemma pair_op (a a' : A) (b b' : B) : (a, b) â‹… (a', b') = (a â‹… a', b â‹… b').
   Proof. done. Qed.
 
   Global Instance prod_cmra_total : CMRATotal A → CMRATotal B → CMRATotal prodR.