diff --git a/CHANGELOG.md b/CHANGELOG.md
index 1c7314b97b14d605352e18f561c41abb99e53c16..a6567f7ae6789ac009baf885ccea7d12d00501a5 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -20,6 +20,8 @@ With this release, we dropped support for Coq 8.9.
   (`iso_cmra_mixin_restrict`) and through an isomorphism (`iso_cmra_mixin`).
 * Add a `frac_agree` library which encapsulates `frac * agree A` for some OFE
   `A`, and provides some useful lemmas.
+* Fix direction of `auth_auth_validN` to make it consistent with similar lemmas,
+  e.g., `auth_auth_valid`. The direction is now `✓{n} (● a) ↔ ✓{n} a`.
 
 **Changes in `proofmode`:**
 
diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v
index 647bf01169c1f2451aa770e68ab9606fce25abe7..a29d6068a6d393367949ee4b1b5fd086cf6ce53e 100644
--- a/theories/algebra/auth.v
+++ b/theories/algebra/auth.v
@@ -162,7 +162,7 @@ Proof.
   - by intros [?[->%(inj to_agree) []]].
   - naive_solver eauto using ucmra_unit_leastN.
 Qed.
-Lemma auth_auth_validN n a : ✓{n} a ↔ ✓{n} (● a).
+Lemma auth_auth_validN n a : ✓{n} (● a) ↔ ✓{n} a.
 Proof.
   rewrite auth_auth_frac_validN -cmra_discrete_valid_iff frac_valid'. naive_solver.
 Qed.