diff --git a/algebra/auth.v b/algebra/auth.v
index d9fa09e152742fe889072b811e75fc6ffa7f44da..301268fbddbbc9dc9c2ee456528ddd87598f0d5b 100644
--- a/algebra/auth.v
+++ b/algebra/auth.v
@@ -191,11 +191,17 @@ Proof.
   exists bf2. rewrite -assoc.
   apply (Hab' _ (Some _)); auto. by rewrite /= assoc.
 Qed.
+
 Lemma auth_update_no_frame a b : a ~l~> b @ Some ∅ → ● a ⋅ ◯ a ~~> ● b ⋅ ◯ b.
 Proof.
   intros. rewrite -{1}(right_id _ _ a) -{1}(right_id _ _ b).
   by apply auth_update.
 Qed.
+Lemma auth_update_no_frag af b : ∅ ~l~> b @ Some af → ● af ~~> ● (b ⋅ af) ⋅ ◯ b.
+Proof.
+  intros. rewrite -{1}(left_id _ _ af) -{1}(right_id _ _ (● _)).
+  by apply auth_update.
+Qed.
 End cmra.
 
 Arguments authR : clear implicits.