diff --git a/iris/algebra/lib/ufrac_auth.v b/iris/algebra/lib/ufrac_auth.v
index 44966f828664a31297d532b0c7ce1431aeb20cd4..12311d84c50c738d969474554e48c1bbcbd6c399 100644
--- a/iris/algebra/lib/ufrac_auth.v
+++ b/iris/algebra/lib/ufrac_auth.v
@@ -9,7 +9,9 @@ difference:
   if we have the authoritative element we can always increase its fraction
   and allocate a new fragment.
 
-  ✓ (a ⋅ b) → ●U_p a ~~> ●U_(p + q) (a ⋅ b) ⋅ ◯U_q b
+<<
+✓ (a ⋅ b) → ●U_p a ~~> ●U_(p + q) (a ⋅ b) ⋅ ◯U_q b
+>>
 
 - We no longer have the [â—¯U{1} a] is the exclusive fragmental element (cf.
   [frac_auth_frag_validN_op_1_l]).