diff --git a/theories/list_numbers.v b/theories/list_numbers.v
index 758f3660546ccf870fc0f64ca1c0500d825b85ff..94d3843f6260bf6d80b6c6000a89b064075f7f1c 100644
--- a/theories/list_numbers.v
+++ b/theories/list_numbers.v
@@ -226,6 +226,10 @@ Section mjoin.
   Implicit Types l k : list A.
   Implicit Types ls : list (list A).
 
+  Lemma join_length ls:
+    length (mjoin ls) = sum_list (length <$> ls).
+  Proof. induction ls; [done|]; csimpl. rewrite app_length. lia. Qed.
+
   Lemma join_lookup_Some ls i x :
     mjoin ls !! i = Some x ↔ ∃ j l i', ls !! j = Some l ∧ l !! i' = Some x
                                      ∧ i = sum_list (length <$> take j ls) + i'.