diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-03-19 14:20:50 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-03-19 14:20:50 -0400 |
| commit | 2c813835518ce6c67c524355977ea22b77438e40 (patch) | |
| tree | 9295de03e67f7c675e4807cee623c4b2c2e2908e /src/Util/ListUtil.v | |
| parent | d635e2e1b8d392644e92f44c5bac3fd2fc24ff36 (diff) | |
Add In_firstn_skipn_split
Diffstat (limited to 'src/Util/ListUtil.v')
| -rw-r--r-- | src/Util/ListUtil.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index 517ab1850..9c5514ccc 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -1152,6 +1152,16 @@ Proof. induction n; destruct l; boring. Qed. +Lemma In_firstn_skipn_split {T} n (x : T) + : forall l, In x l -> In x (firstn n l) \/ In x (skipn n l). +Proof. + induction n; destruct l; boring. + match goal with + | [ IH : forall l, In ?x l -> _ \/ _, H' : In ?x ?ls |- _ ] + => destruct (IH _ H') + end; auto. +Qed. + Lemma firstn_firstn_min : forall {A} m n (l : list A), firstn n (firstn m l) = firstn (min n m) l. Proof. |