diff --git a/CHANGELOG.md b/CHANGELOG.md
index 9b87bae3ebb6ab058ef8118abdd0215732452927..601a57ecb94c3fe2fa7eee3b007793a4efb2be93 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -152,6 +152,7 @@ API-breaking change is listed.
   `map_filter_singleton_False`, `map_filter_comm`, `map_union_least`,
   `map_subseteq_difference_l`, `insert_difference`, `insert_difference'`,
   `difference_insert`, `difference_insert_subseteq`. (by Hai Dang)
+- Add `map_size_disj_union`.
 - Tweak reduction on `gset`, so that `cbn` matches the behavior by `simpl` and
   does not unfold `gset` operations. (by Paolo G. Giarrusso, BedRock Systems)
 - Add `get_head` tactic to determine the syntactic head of a function
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 8bbcffa18b8e2386d2c106cbcdb48dbe795e3ccc..8b0a6ea3e5041846bb0719b4547c6b52dfd9c132 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -2294,6 +2294,19 @@ Proof.
   destruct (m1 !! i), (m2 !! i); simpl; repeat (destruct (f _)); naive_solver.
 Qed.
 
+Lemma map_size_disj_union {A} (m1 m2 : M A) :
+  m1 ##ₘ m2 → size (m1 ∪ m2) = size m1 + size m2.
+Proof.
+  intros Hdisj. induction m1 as [|k x m1 Hm1 IH] using map_ind.
+  { rewrite (left_id _ _), map_size_empty. done. }
+  rewrite <-insert_union_l.
+  rewrite map_size_insert.
+  rewrite lookup_union_r by done.
+  apply map_disjoint_insert_l in Hdisj as [-> Hdisj].
+  rewrite map_size_insert, Hm1.
+  rewrite IH by done. done.
+Qed.
+
 Lemma map_cross_split {A} (ma mb mc md : M A) :
   ma ##ₘ mb → mc ##ₘ md →
   ma ∪ mb = mc ∪ md →