diff --git a/CHANGELOG.md b/CHANGELOG.md
index d5e6f775519eccc650176025e7160d1bafff5d26..a604255c99d28516e1c3be1a0e2e1f579e5d7e0d 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -27,6 +27,7 @@ Coq 8.19 is newly supported by this version of std++.
   These tactics support both named hypotheses (`inv H`) and using a number
   to refer to a hypothesis on the goal (`inv 1`).
 - Add `prod_swap : A * B → B * A` and some basic theory about it.
+- Add lemma `join_app`.
 
 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/stdpp/list.v b/stdpp/list.v
index 38e225dbd7f0d90261a6cd15454a80ae77bc9833..a146fcce440f21e8e2699629440dd03fc693be36 100644
--- a/stdpp/list.v
+++ b/stdpp/list.v
@@ -4366,6 +4366,13 @@ Section ret_join.
   Proof. by rewrite join_nil. Qed.
   Lemma join_nil_2 (ls : list (list A)) : Forall (.= []) ls → mjoin ls = [].
   Proof. by rewrite join_nil. Qed.
+
+  Lemma join_app (l1 l2 : list (list A)) :
+    mjoin (l1 ++ l2) = mjoin l1 ++ mjoin l2.
+  Proof.
+    induction l1 as [|x l1 IH]; simpl; [done|]. by rewrite <-(assoc_L _ _), IH.
+  Qed.
+
   Lemma Forall_join (P : A → Prop) (ls: list (list A)) :
     Forall (Forall P) ls → Forall P (mjoin ls).
   Proof. induction 1; simpl; auto using Forall_app_2. Qed.