Merge pull request #75 from NicholasBHubbard/add-lemma-length_app_comm

add lemma length_app_comm

Author: proux01

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).

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.