diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v
index 4e1e9ddde428d3976e273fbad13a4e9698a5fa1e..6466762915684d38c6a625777abb32f528a1d4b6 100644
--- a/theories/algebra/auth.v
+++ b/theories/algebra/auth.v
@@ -366,6 +366,12 @@ Qed.
 Lemma auth_update_alloc a a' b' : (a,ε) ~l~> (a',b') → ● a ~~> ● a' ⋅ ◯ b'.
 Proof. intros. rewrite -(right_id _ _ (● a)). by apply auth_update. Qed.
 
+Lemma auth_update_auth a a' b' : (a,ε) ~l~> (a',b') → ● a ~~> ● a'.
+Proof.
+  intros. etrans; first exact: auth_update_alloc.
+  exact: cmra_update_op_l.
+Qed.
+
 Lemma auth_update_core_id a b `{!CoreId b} :
   b ≼ a → ● a ~~> ● a ⋅ ◯ b.
 Proof.
diff --git a/theories/algebra/updates.v b/theories/algebra/updates.v
index 790017571c14fd552c363d01d69354a15d4ed0c2..4e1f96c720619eb406872ade12a1e65bd92e397a 100644
--- a/theories/algebra/updates.v
+++ b/theories/algebra/updates.v
@@ -47,6 +47,11 @@ Qed.
 Lemma cmra_updateP_weaken (P Q : A → Prop) x :
   x ~~>: P → (∀ y, P y → Q y) → x ~~>: Q.
 Proof. eauto using cmra_updateP_compose, cmra_updateP_id. Qed.
+Lemma cmra_update_exclusive `{!Exclusive x} y:
+  ✓ y → x ~~> y.
+Proof. move=>??[z|]=>[/exclusiveN_l[]|_]. by apply cmra_valid_validN. Qed.
+
+(** Updates form a preorder. *)
 Global Instance cmra_update_preorder : PreOrder (@cmra_update A).
 Proof.
   split.
@@ -54,9 +59,6 @@ Proof.
   - intros x y z. rewrite !cmra_update_updateP.
     eauto using cmra_updateP_compose with subst.
 Qed.
-Lemma cmra_update_exclusive `{!Exclusive x} y:
-  ✓ y → x ~~> y.
-Proof. move=>??[z|]=>[/exclusiveN_l[]|_]. by apply cmra_valid_validN. Qed.
 
 Lemma cmra_updateP_op (P1 P2 Q : A → Prop) x1 x2 :
   x1 ~~>: P1 → x2 ~~>: P2 → (∀ y1 y2, P1 y1 → P2 y2 → Q (y1 ⋅ y2)) →