Require Import List.

Lemma skipn_app {A}:
  forall (l1 l2: list A) n,
    n <= List.length l1 ->
    skipn n (List.app l1 l2) =
    List.app (skipn n l1) l2.
A:Type
forall (l1 l2 : list A) (n : nat),
n <= length l1 ->
skipn n (l1 ++ l2) = skipn n l1 ++ l2
Proof.
A:Type
forall (l1 l2 : list A) (n : nat),
n <= length l1 ->
skipn n (l1 ++ l2) = skipn n l1 ++ l2
  induction l1.
A:Type
forall (l2 : list A) (n : nat),
n <= length nil ->
skipn n (nil ++ l2) = skipn n nil ++ l2
A:Type
a:A
l1:list A
IHl1:forall (l2 : list A) (n : nat),
n <= length l1 ->
skipn n (l1 ++ l2) = skipn n l1 ++ l2
forall (l2 : list A) (n : nat),
n <= length (a :: l1) ->
skipn n ((a :: l1) ++ l2) = skipn n (a :: l1) ++ l2
  -
A:Type
forall (l2 : list A) (n : nat),
n <= length nil ->
skipn n (nil ++ l2) = skipn n nil ++ l2 destruct n.
A:Type
l2:list A
0 <= length nil ->
skipn 0 (nil ++ l2) = skipn 0 nil ++ l2
A:Type
l2:list A
n:nat
S n <= length nil ->
skipn (S n) (nil ++ l2) = skipn (S n) nil ++ l2
    all: cbn.
A:Type
l2:list A
0 <= 0 -> l2 = l2
A:Type
l2:list A
n:nat
S n <= 0 ->
match l2 with
| nil => nil
| _ :: l => skipn n l
end = l2
    +
A:Type
l2:list A
0 <= 0 -> l2 = l2 reflexivity.
    +
A:Type
l2:list A
n:nat
S n <= 0 ->
match l2 with
| nil => nil
| _ :: l => skipn n l
end = l2 inversion 1.
  -
A:Type
a:A
l1:list A
IHl1:forall (l2 : list A) (n : nat),
n <= length l1 ->
skipn n (l1 ++ l2) = skipn n l1 ++ l2
forall (l2 : list A) (n : nat),
n <= length (a :: l1) ->
skipn n ((a :: l1) ++ l2) = skipn n (a :: l1) ++ l2 destruct n.
A:Type
a:A
l1:list A
IHl1:forall (l2 : list A) (n : nat),
n <= length l1 ->
skipn n (l1 ++ l2) = skipn n l1 ++ l2
l2:list A
0 <= length (a :: l1) ->
skipn 0 ((a :: l1) ++ l2) = skipn 0 (a :: l1) ++ l2
A:Type
a:A
l1:list A
IHl1:forall (l2 : list A) (n : nat),
n <= length l1 ->
skipn n (l1 ++ l2) = skipn n l1 ++ l2
l2:list A
n:nat
S n <= length (a :: l1) ->
skipn (S n) ((a :: l1) ++ l2) =
skipn (S n) (a :: l1) ++ l2 cbn.
A:Type
a:A
l1:list A
IHl1:forall (l2 : list A) (n : nat),
n <= length l1 ->
skipn n (l1 ++ l2) = skipn n l1 ++ l2
l2:list A
0 <= S (length l1) -> a :: l1 ++ l2 = a :: l1 ++ l2
A:Type
a:A
l1:list A
IHl1:forall (l2 : list A) (n : nat),
n <= length l1 ->
skipn n (l1 ++ l2) = skipn n l1 ++ l2
l2:list A
n:nat
S n <= length (a :: l1) ->
skipn (S n) ((a :: l1) ++ l2) =
skipn (S n) (a :: l1) ++ l2
    +
A:Type
a:A
l1:list A
IHl1:forall (l2 : list A) (n : nat),
n <= length l1 ->
skipn n (l1 ++ l2) = skipn n l1 ++ l2
l2:list A
0 <= S (length l1) -> a :: l1 ++ l2 = a :: l1 ++ l2 reflexivity.
    +
A:Type
a:A
l1:list A
IHl1:forall (l2 : list A) (n : nat),
n <= length l1 ->
skipn n (l1 ++ l2) = skipn n l1 ++ l2
l2:list A
n:nat
S n <= length (a :: l1) ->
skipn (S n) ((a :: l1) ++ l2) =
skipn (S n) (a :: l1) ++ l2 intros.
A:Type
a:A
l1:list A
IHl1:forall (l2 : list A) (n : nat),
n <= length l1 ->
skipn n (l1 ++ l2) = skipn n l1 ++ l2
l2:list A
n:nat
H:S n <= length (a :: l1)
skipn (S n) ((a :: l1) ++ l2) =
skipn (S n) (a :: l1) ++ l2 apply IHl1.
A:Type
a:A
l1:list A
IHl1:forall (l2 : list A) (n : nat),
n <= length l1 ->
skipn n (l1 ++ l2) = skipn n l1 ++ l2
l2:list A
n:nat
H:S n <= length (a :: l1)
n <= length l1
      Check le_S_n.
le_S_n
     : forall n m : nat, S n <= S m -> n <= m
A:Type
a:A
l1:list A
IHl1:forall (l2 : list A) (n : nat),
n <= length l1 ->
skipn n (l1 ++ l2) = skipn n l1 ++ l2
l2:list A
n:nat
H:S n <= length (a :: l1)
n <= length l1
      apply le_S_n.
A:Type
a:A
l1:list A
IHl1:forall (l2 : list A) (n : nat),
n <= length l1 ->
skipn n (l1 ++ l2) = skipn n l1 ++ l2
l2:list A
n:nat
H:S n <= length (a :: l1)
S n <= S (length l1)
      match goal with
      | [ H: _ <= _ |- _ ] => simpl in H
      end.
A:Type
a:A
l1:list A
IHl1:forall (l2 : list A) (n : nat),
n <= length l1 ->
skipn n (l1 ++ l2) = skipn n l1 ++ l2
l2:list A
n:nat
H:S n <= S (length l1)
S n <= S (length l1)
      assumption.
Qed.