Add skipn_skipn

1 files changed, 13 insertions, 1 deletions

diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v
index 4d6555778..eb807abda 100644
--- a/src/Util/ListUtil.v
+++ b/src/Util/ListUtil.v
@@ -765,6 +765,18 @@ Qed.
 
 Hint Rewrite @skipn_app : push_skipn.
 
+Lemma skipn_skipn {A} n1 n2 (ls : list A)
+  : skipn n2 (skipn n1 ls) = skipn (n1 + n2) ls.
+Proof.
+  revert n2 ls; induction n1, ls;
+    simpl; autorewrite with simpl_skipn;
+      boring.
+Qed.
+
+Hint Rewrite @skipn_skipn : simpl_skipn.
+Hint Rewrite <- @skipn_skipn : push_skipn.
+Hint Rewrite @skipn_skipn : pull_skipn.
+
 Lemma firstn_app_inleft : forall {A} n (xs ys : list A), (n <= length xs)%nat ->
   firstn n (xs ++ ys) = firstn n xs.
 Proof.
@@ -1671,4 +1683,4 @@ Lemma map2_map {A B C A' B'} (f:A -> B -> C) (g:A' -> A) (h:B' -> B) (xs:list A'
 Proof.
   revert ys; induction xs; destruct ys; intros; try reflexivity; [].
   simpl. rewrite IHxs. reflexivity.
-Qed.
\ No newline at end of file
+Qed.