diff --git a/CHANGELOG.md b/CHANGELOG.md
index beadd84c7496c9ab623105a76bcc431fed0caeb5..785e0ffe7979db0e37d1d21c92da64a5692a8a05 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -26,6 +26,7 @@ Coq 8.11 is no longer supported.
 - Add `map_Exists` as an analogue to `map_Forall`. (by Michael Sammler)
 - Add `case_match eqn:H` that behaves like `case_match` but allows naming the
   generated equality. (by Michael Sammler)
+- Flip direction of `map_disjoint_fmap`.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index d4dd56acc20d7634b4265659ea458162a41d2b08..c07f7aaa880160321e4d09ace1124c7af4533559 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -2054,7 +2054,7 @@ Proof.
 Qed.
 
 Lemma map_disjoint_fmap {A B} (f1 f2 : A → B) (m1 m2 : M A) :
-  m1 ##ₘ m2 ↔ f1 <$> m1 ##ₘ f2 <$> m2.
+  f1 <$> m1 ##ₘ f2 <$> m2 ↔ m1 ##ₘ m2.
 Proof.
   rewrite !map_disjoint_spec. setoid_rewrite lookup_fmap_Some. naive_solver.
 Qed.