diff --git a/theories/algebra/frac_auth.v b/theories/algebra/frac_auth.v
index fdee147fee6c66e0285797c060a0fd28f7b98690..08fc6f9e00c3905e205bfdb7ceef0aa23d2be73f 100644
--- a/theories/algebra/frac_auth.v
+++ b/theories/algebra/frac_auth.v
@@ -105,4 +105,9 @@ Section frac_auth.
   Proof.
     intros. by apply auth_update, option_local_update, prod_local_update_2.
   Qed.
+
+  Lemma frac_auth_update_1 a b a' : ✓ a' → ●! a ⋅ ◯! b ~~> ●! a' ⋅ ◯! a'.
+  Proof.
+    intros. by apply auth_update, option_local_update, exclusive_local_update.
+  Qed.
 End frac_auth.