diff --git a/algebra/auth.v b/algebra/auth.v
index 482b1eb943bf75c3db5d1e02c254f7acc10cecd1..f6a5ae88df9ab3a35ccd3759502aeb8df92c8039 100644
--- a/algebra/auth.v
+++ b/algebra/auth.v
@@ -193,7 +193,7 @@ Lemma auth_validI {M} (x : auth A) :
           end : uPred M).
 Proof. uPred.unseal. by destruct x as [[[]|]]. Qed.
 
-Lemma auth_frag_op a b : ◯ (a ⋅ b) ≡ ◯ a ⋅ ◯ b.
+Lemma auth_frag_op a b : â—¯ (a â‹… b) = â—¯ a â‹… â—¯ b.
 Proof. done. Qed.
 Lemma auth_frag_mono a b : a ≼ b → ◯ a ≼ ◯ b.
 Proof. intros [c ->]. rewrite auth_frag_op. apply cmra_included_l. Qed.