add lemma length_app_comm

Author: NicholasBHubbard

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.
@@ -3972,6 +3980,7 @@ Global Hint Rewrite
   length_map (* length (map f l) = length l *)
   length_seq (* length (seq start len) = len *)
   length_app (* length (l ++ l') = length l + length l' *)
+  length_app_comm (* length (l ++ l') = length (l' ++ l) *)
   length_rev (* length (rev l) = length l *)
   app_nil_r (* l ++ nil = l *)
   : list.