diff --git a/doc/changelog/01-added/75-add-length_app_comm.rst b/doc/changelog/01-added/75-add-length_app_comm.rst
new file mode 100644
index 0000000000..7ef87fdb90
--- /dev/null
+++ b/doc/changelog/01-added/75-add-length_app_comm.rst
@@ -0,0 +1,5 @@
+- in `List.v`
+
+  + lemma `length_app_comm`
+    (`#75 <https://github.com/coq/stdlib/pull/75>`_,
+    by Nicholas Hubbard).
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index 916d97ba42..813402f2ae 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -239,6 +239,14 @@ Section Facts.
     intro l; induction l; simpl; auto.
   Qed.
 
+  Lemma length_app_comm : forall l l' : list A, length (l++l') = length (l'++l).
+  Proof.
+    intros.
+    repeat rewrite length_app.
+    rewrite Nat.add_comm.
+    reflexivity.
+  Qed.
+
   Lemma last_length : forall (l : list A) a, length (l ++ [a]) = S (length l).
   Proof.
     intros ; rewrite length_app ; simpl.