From b2e1bc62fc9d572c0a5cb57953b12c7a0ceace4b Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Tue, 14 Mar 2017 21:09:16 -0400
Subject: Add skipn_skipn

---
 src/Util/ListUtil.v | 14 +++++++++++++-
 1 file changed, 13 insertions(+), 1 deletion(-)

(limited to 'src/Util/ListUtil.v')

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.
-- 
cgit v1.2.3