(** * Addendum to the standard library of Coq *)

Require Import Bool Arith Div2 List Permutation.
Require Export Omega.

Global Obligation Tactic := idtac.

Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) .. ).

Lemma length_nil : forall A (l : list A),
  length l = 0 -> l = nil.
Proof.
(* Goal: forall (A : Type) (l : list A) (_ : @eq nat (@length A l) O), @eq (list A) l (@nil A) *)
 intros; destruct l; trivial; intros.
(* Goal: @eq (list A) (@cons A a l) (@nil A) *)
 simpl in H; contradict H; omega.
Qed.

Lemma length_tail A l : length (@tail A l) = length l - 1.
Proof.
(* Goal: @eq nat (@length A (@tl A l)) (Init.Nat.sub (@length A l) (S O)) *)
  destruct l; simpl; auto with arith.
Qed.

Lemma hd_nth_0 A (l : list A) d :
  hd d l = nth 0 l d.
Proof. intros; case l; simpl; trivial. Qed.

Lemma hd_nth_1 A (l : list A) d :
  hd d (tl l) = nth 1 l d.
Proof.
(* Goal: @eq A (@hd A d (@tl A l)) (@nth A (S O) l d) *)
 intros; case l; simpl; intros; trivial.
(* Goal: @eq A (@hd A d l0) (@nth A O l0 d) *)
 apply hd_nth_0.
Qed.

Lemma In_hd (A : Type)(d:A)(l : list A)(n : nat)(H : length l = S n) :
  In (hd d l) l.
Proof.
(* Goal: @In A (@hd A d l) l *)
destruct l.
(* Goal: @In A (@hd A d (@nil A)) (@nil A) *)
(* Goal: @In A (@hd A d (@cons A a l)) (@cons A a l) *)
simpl in H.
(* Goal: @In A (@hd A d (@nil A)) (@nil A) *)
(* Goal: @In A (@hd A d (@cons A a l)) (@cons A a l) *)
discriminate H.
(* Goal: @In A (@hd A d (@cons A a l)) (@cons A a l) *)
simpl; tauto.
Qed.

Lemma map_hd : forall A B (f:A->B) d l, f (hd d l) = hd (f d) (map f l).
Proof.
(* Goal: forall (A B : Type) (f : forall _ : A, B) (d : A) (l : list A), @eq B (f (@hd A d l)) (@hd B (f d) (@map A B f l)) *)
intros A B f d [ | x l]; trivial.
Qed.

Lemma map_tl : forall A B (f:A->B) l, map f (tl l) = tl (map f l).
Proof.
intros A B f [ | x l]; trivial.
Qed.

Lemma map_eq_hd :
  forall A B (f:A->B) d l1 l2,
  map f l1 = map f l2 -> f (hd d l1) = f (hd d l2).
Proof.
(* Goal: forall (A B : Type) (f : forall _ : A, B) (d : A) (l1 l2 : list A) (_ : @eq (list B) (@map A B f l1) (@map A B f l2)), @eq B (f (@hd A d l1)) (f (@hd A d l2)) *)
intros A B f d [ | a1 l1] [ | a2 l2]; simpl; congruence.
Qed.

Lemma firstn_nil {A} n : firstn n (@nil A) = nil.
Proof. case n; simpl; trivial. Qed.

Lemma skipn_nil : forall {A} n (x : list A),
  length x <= n -> skipn n x = nil.
Proof.
(* Goal: forall (A : Type) (n : nat) (x : list A) (_ : le (@length A x) n), @eq (list A) (@skipn A n x) (@nil A) *)
  induction n; simpl in *; trivial; intros.
(* Goal: @eq (list A) x (@nil A) *)
(* Goal: @eq (list A) match x with | nil => @nil A | cons a l => @skipn A n l end (@nil A) *)
  apply length_nil; auto; omega.
(* Goal: @eq (list A) match x with | nil => @nil A | cons a l => @skipn A n l end (@nil A) *)
  destruct x; simpl in *; trivial.
(* Goal: @eq (list A) (@skipn A n x) (@nil A) *)
  apply IHn; omega.
Qed.

Lemma nth_firstn : forall A i j (l:list A) d,
  i < j -> nth i (firstn j l) d = nth i l d.
Proof.
(* Goal: forall (A : Type) (i j : nat) (l : list A) (d : A) (_ : lt i j), @eq A (@nth A i (@firstn A j l) d) (@nth A i l d) *)
 intros A i j.
(* Goal: forall (l : list A) (d : A) (_ : lt i j), @eq A (@nth A i (@firstn A j l) d) (@nth A i l d) *)
 revert i; induction j; simpl; intros.
(* Goal: @eq (list A) (@nil A) (@cons A d (@nil A)) *)
(* Goal: @eq (list A) (@skipn A n y) (@cons A (@nth A n y d) match y with | nil => @nil A | cons a l => @skipn A n l end) *)
 contradict H; omega.
(* Goal: @eq A (@nth A i match l with | nil => @nil A | cons a l => @cons A a (@firstn A j l) end d) (@nth A i l d) *)
 case l; simpl; destruct i; simpl; trivial; intros.
(* Goal: @eq A (@nth A i (@firstn A j l0) d) (@nth A i l0 d) *)
 apply IHj; omega.
Qed.

Lemma nth_skipn A i j (l:list A) d : 
  nth i (skipn j l) d = nth (j+i) l d.
Proof.
(* Goal: @eq A (@nth A i (@skipn A j l) d) (@nth A (Init.Nat.add j i) l d) *)
 intros; revert i l.
(* Goal: forall (i : nat) (l : list A), @eq A (@nth A i (@skipn A j l) d) (@nth A (Init.Nat.add j i) l d) *)
 induction j; simpl; intros; trivial.
(* Goal: @eq A (@nth A i match l with | nil => @nil A | cons a l => @skipn A j l end d) (@nth A (S (Init.Nat.add j i)) l d) *)
 destruct l; simpl; trivial; case i; trivial.
Qed.

Lemma length_skipn : forall A n (y : list A),
  length (skipn n y) = length y - n.
Proof.
(* Goal: forall (A : Type) (n : nat) (y : list A), @eq nat (@length A (@skipn A n y)) (Init.Nat.sub (@length A y) n) *)
  induction n; simpl; intros; [ omega | ].
(* Goal: @eq nat (@length A match y with | nil => @nil A | cons a l => @skipn A n l end) (Init.Nat.sub (@length A y) (S n)) *)
  destruct y; simpl; trivial.
Qed.

Lemma skipn_length : forall {A} n (l:list A), 
  length (skipn n l) = length l - n.
Proof.
(* Goal: forall (A : Type) (n : nat) (l : list A), @eq nat (@length A (@skipn A n l)) (Init.Nat.sub (@length A l) n) *)
  induction n; simpl; intros; auto with arith.
(* Goal: @eq nat (@length A match l with | nil => @nil A | cons a l => @skipn A n l end) (Init.Nat.sub (@length A l) (S n)) *)
  destruct l; simpl; auto.
Qed.

Lemma cons_skipn :
  forall A d i (l:list A),
  i < length l ->
  nth i l d :: skipn (S i) l = skipn i l.
Proof.
(* Goal: forall (A : Type) (d : A) (i : nat) (l : list A) (_ : lt i (@length A l)), @eq (list A) (@cons A (@nth A i l d) (@skipn A (S i) l)) (@skipn A i l) *)
 induction i as [ | i IH]; simpl; intros.
(* Goal: @eq (list A) (@cons A (@nth A O l d) match l with | nil => @nil A | cons a l => l end) l *)
(* Goal: @eq (list A) (@cons A (@nth A (S i) l d) match l with | nil => @nil A | cons a (nil as l) => @nil A | cons a (cons a0 l0 as l) => @skipn A i l0 end) match l with | nil => @nil A | cons a l => @skipn A i l end *)
 destruct l as [ | x l]; trivial.
(* Goal: @eq (list A) (@cons A (@nth A (S i) (@nil A) d) (@nil A)) (@nil A) *)
(* Goal: @eq (list A) (@cons A (@nth A (S i) (@cons A x l) d) match l with | nil => @nil A | cons a l => @skipn A i l end) (@skipn A i l) *)
 contradict H; simpl; omega.
(* Goal: @eq (list A) (@cons A (@nth A (S i) l d) match l with | nil => @nil A | cons a (nil as l) => @nil A | cons a (cons a0 l0 as l) => @skipn A i l0 end) match l with | nil => @nil A | cons a l => @skipn A i l end *)
 destruct l as [ | x l].
(* Goal: @eq (list A) (@cons A (@nth A (S i) (@nil A) d) (@nil A)) (@nil A) *)
(* Goal: @eq (list A) (@cons A (@nth A (S i) (@cons A x l) d) match l with | nil => @nil A | cons a l => @skipn A i l end) (@skipn A i l) *)
 contradict H; simpl; omega.
(* Goal: @eq (list A) (@cons A (@nth A (S i) (@cons A x l) d) match l with | nil => @nil A | cons a l => @skipn A i l end) (@skipn A i l) *)
 rewrite <- IH; trivial.
(* Goal: lt i (@length A l) *)
 simpl in H; omega.
Qed.

Lemma skipn_plus :
  forall A j i (l:list A), skipn (i+j) l = skipn i (skipn j l).
Proof.
(* Goal: forall (A : Type) (j i : nat) (l : list A), @eq (list A) (@skipn A (Init.Nat.add i j) l) (@skipn A i (@skipn A j l)) *)
 induction j as [ | j IH]; simpl; intros.
(* Goal: @eq (list nat) (@cons nat start (seq (S start) len)) (@cons nat (Init.Nat.add start O) (seq (S (Init.Nat.add start O)) len)) *)
(* Goal: @eq (list nat) (@skipn nat n0 (seq (S start) len)) (seq (Init.Nat.add start (S n0)) (Init.Nat.sub len n0)) *)
 rewrite plus_0_r; trivial.
(* Goal: @eq (list A) (@skipn A (Init.Nat.add i (S j)) l) (@skipn A i match l with | nil => @nil A | cons a l => @skipn A j l end) *)
 rewrite <- plus_Snm_nSm.
(* Goal: @eq (list A) (@skipn A (Init.Nat.add (S i) j) l) (@skipn A i match l with | nil => @nil A | cons a l => @skipn A j l end) *)
 case l.
(* Goal: @eq (list A) (@skipn A (Init.Nat.add (S i) j) (@nil A)) (@skipn A i (@nil A)) *)
(* Goal: forall (a : A) (l : list A), @eq (list A) (@skipn A (Init.Nat.add (S i) j) (@cons A a l)) (@skipn A i (@skipn A j l)) *)
 rewrite !skipn_nil; simpl; trivial; omega.
(* Goal: forall (a : A) (l : list A), @eq (list A) (@skipn A (Init.Nat.add (S i) j) (@cons A a l)) (@skipn A i (@skipn A j l)) *)
 simpl; trivial.
Qed.

Lemma skipn_hd : forall {A} n y (d:A), 
  n < length y -> 
  skipn n y = nth n y d :: skipn (S n) y.
Proof.
(* Goal: forall (A : Type) (n : nat) (y : list A) (d : A) (_ : lt n (@length A y)), @eq (list A) (@skipn A n y) (@cons A (@nth A n y d) (@skipn A (S n) y)) *)
 induction n; simpl; intros.
(* Goal: @eq (list A) y (@cons A (@nth A O y d) match y with | nil => @nil A | cons a l => l end) *)
(* Goal: @eq (list A) match y with | nil => @nil A | cons a l => @skipn A n l end (@cons A (@nth A (S n) y d) match y with | nil => @nil A | cons a (nil as l) => @nil A | cons a (cons a0 l0 as l) => @skipn A n l0 end) *)
 destruct y; simpl in *; trivial.
(* Goal: @eq (list A) (@nil A) (@cons A d (@nil A)) *)
(* Goal: @eq (list A) (@skipn A n y) (@cons A (@nth A n y d) match y with | nil => @nil A | cons a l => @skipn A n l end) *)
 contradict H; omega.
(* Goal: @eq (list A) match y with | nil => @nil A | cons a l => @skipn A n l end (@cons A (@nth A (S n) y d) match y with | nil => @nil A | cons a (nil as l) => @nil A | cons a (cons a0 l0 as l) => @skipn A n l0 end) *)
 destruct y; simpl in *.
(* Goal: @eq (list A) (@nil A) (@cons A d (@nil A)) *)
(* Goal: @eq (list A) (@skipn A n y) (@cons A (@nth A n y d) match y with | nil => @nil A | cons a l => @skipn A n l end) *)
 contradict H; omega.
(* Goal: @eq (list A) (@skipn A n y) (@cons A (@nth A n y d) match y with | nil => @nil A | cons a l => @skipn A n l end) *)
 apply IHn.
(* Goal: le i (@length A l) *)
 omega.
Qed.

Lemma firstn_app {A} (l l' : list A) : 
  firstn (length l) (l ++ l') = l.
Proof.
(* Goal: forall (a : A) (l : list A), @eq (list A) (@skipn A (Init.Nat.add (S i) j) (@cons A a l)) (@skipn A i (@skipn A j l)) *)
 induction l; intros; simpl; trivial.
(* Goal: @eq (list A) (@cons A a (@firstn A (@length A l) (@app A l l'))) (@cons A a l) *)
 rewrite IHl; trivial.
Qed.

Lemma skipn_app {A} (l l' : list A) : 
  skipn (length l) (l ++ l') = l'.
Proof. induction l; intros; simpl; trivial. Qed.

Lemma map_cons : forall A B (f:A->B) a l, map f (a::l) = f a :: map f l.
Proof. trivial. Qed.

Lemma map_firstn : forall A B (f:A->B) n l,
  map f (firstn n l) = firstn n (map f l).
Proof.
(* Goal: @eq (list A) l l *)
 induction n; simpl; intros; trivial.
(* Goal: @eq (list B) (@map A B f match l with | nil => @nil A | cons a l => @skipn A n l end) match @map A B f l with | nil => @nil B | cons a l => @skipn B n l end *)
 case l; simpl; trivial; congruence.
Qed.

Lemma map_skipn : forall A B (f:A->B) n l,
  map f (skipn n l) = skipn n (map f l).
Proof.
(* Goal: @eq (list A) l l *)
 induction n; simpl; intros; trivial.
(* Goal: @eq (list B) (@map A B f match l with | nil => @nil A | cons a l => @skipn A n l end) match @map A B f l with | nil => @nil B | cons a l => @skipn B n l end *)
 case l; simpl; trivial; congruence.
Qed.

Lemma map_nth_seq : forall A (l:list A) len n d,
  length l = len + n ->
  map (fun x : nat => nth x l d) (seq n len) = (skipn n l).
Proof.
(* Goal: forall (A : Type) (l : list A) (len n : nat) (d : A) (_ : @eq nat (@length A l) (Init.Nat.add len n)), @eq (list A) (@map nat A (fun x : nat => @nth A x l d) (seq n len)) (@skipn A n l) *)
 intros A l len; revert l.
(* Goal: forall n start : nat, @eq (list nat) (@skipn nat n (seq start len)) (seq (Init.Nat.add start n) (Init.Nat.sub len n)) *)
 induction len; simpl; intros.
(* Goal: le i (@length A l) *)
 rewrite skipn_nil; trivial; omega.
(* Goal: le i (@length A l) *)
 rewrite IHlen, <- skipn_hd; trivial; omega.
Qed.

Lemma skipn_nil_length : forall A n (l : list A),
  skipn n l = nil -> length l <= n.
Proof.
(* Goal: forall (A : Type) (n : nat) (l : list A) (_ : @eq (list A) (@skipn A n l) (@nil A)), le (@length A l) n *)
  induction n; simpl in *; intros.
(* Goal: forall (a : A) (l : list A), @eq (list A) (@skipn A (Init.Nat.add (S i) j) (@cons A a l)) (@skipn A i (@skipn A j l)) *)
  subst; simpl; trivial.
(* Goal: le (@length A l) (S n) *)
  destruct l; simpl; [ omega | ].
(* Goal: le i (@length A l) *)
  generalize (IHn _ H); omega.
Qed.

Lemma firstn_map_nth :
  forall A d n m (l:list A),
  m+n <= length l ->
  firstn n (skipn m l) = map (fun i => nth i l d) (seq m n).
Proof.
(* Goal: @eq (list A) l l *)
 induction n as [ | n IH]; simpl; intros; trivial.
(* Goal: le i (@length A l) *)
 rewrite <- IH by omega.
 replace (skipn (S m) l) with (tl (skipn m l)).
 case_eq (skipn m l).
 intro H0.
 contradict H0.
(* Goal: @eq A match i with | O => d | S m => d end x *)
(* Goal: @eq A match i with | O => x | S m => @nth A m (@repeat A n x) d end x *)
 contradict H.
(* Goal: le i (@length A l) *)
 apply skipn_nil_length in H; omega.
 intros x l' H0; simpl; f_equal.
 erewrite skipn_hd in H0.
 injection H0.
 intros _ H1.
 symmetry; apply H1.
(* Goal: le i (@length A l) *)
 omega.
(* Goal: le i (@length A l) *)
 rewrite <- cons_skipn with (d:=d); trivial; omega.
Qed.

Lemma firstn_seq n start len :
  firstn n (seq start len) = seq start (min n len).
Proof.
(* Goal: @eq (list nat) (@skipn nat n (seq start len)) (seq (Init.Nat.add start n) (Init.Nat.sub len n)) *)
 intros; revert n start.
(* Goal: forall n start : nat, @eq (list nat) (@skipn nat n (seq start len)) (seq (Init.Nat.add start n) (Init.Nat.sub len n)) *)
 induction len; simpl; intros.
(* Goal: @eq (list nat) (@firstn nat n (@nil nat)) (seq start (Init.Nat.min n O)) *)
(* Goal: @eq (list nat) (@firstn nat n (@cons nat start (seq (S start) len))) (seq start (Init.Nat.min n (S len))) *)
 rewrite min_r; simpl;[ | omega].
(* Goal: @eq (list nat) (@firstn nat n (@nil nat)) (@nil nat) *)
(* Goal: @eq (list nat) (@firstn nat n (@cons nat start (seq (S start) len))) (seq start (Init.Nat.min n (S len))) *)
 apply firstn_nil.
(* Goal: @eq (list nat) (@firstn nat n (@cons nat start (seq (S start) len))) (seq start (Init.Nat.min n (S len))) *)
 case n; simpl; trivial; congruence.
Qed.

Lemma skipn_seq n start len :
  skipn n (seq start len) = seq (start+n) (len-n).
Proof.
(* Goal: @eq (list nat) (@skipn nat n (seq start len)) (seq (Init.Nat.add start n) (Init.Nat.sub len n)) *)
 intros; revert n start.
(* Goal: forall n start : nat, @eq (list nat) (@skipn nat n (seq start len)) (seq (Init.Nat.add start n) (Init.Nat.sub len n)) *)
 induction len; simpl; intros.
(* Goal: le i (@length A l) *)
 apply skipn_nil; simpl; omega.
(* Goal: @eq (list nat) (@skipn nat n (@cons nat start (seq (S start) len))) (seq (Init.Nat.add start n) match n with | O => S len | S l => Init.Nat.sub len l end) *)
 case n; simpl; intros.
(* Goal: @eq (list nat) (@cons nat start (seq (S start) len)) (@cons nat (Init.Nat.add start O) (seq (S (Init.Nat.add start O)) len)) *)
(* Goal: @eq (list nat) (@skipn nat n0 (seq (S start) len)) (seq (Init.Nat.add start (S n0)) (Init.Nat.sub len n0)) *)
 rewrite plus_0_r; trivial.
(* Goal: @eq (list nat) (@skipn nat n0 (seq (S start) len)) (seq (Init.Nat.add start (S n0)) (Init.Nat.sub len n0)) *)
 rewrite <- plus_Snm_nSm; apply IHlen.
Qed.

Lemma in_seq_iff : forall x len start,
  In x (seq start len) <-> start <= x < start+len.
Proof.
(* Goal: forall x len start : nat, iff (@In nat x (seq start len)) (and (le start x) (lt x (Init.Nat.add start len))) *)
intros x len.
(* Goal: forall start : nat, iff (@In nat x (seq start len)) (and (le start x) (lt x (Init.Nat.add start len))) *)
induction len; simpl; intros;[ omega | ].
(* Goal: iff (@In A x (@app A (@firstn A i l) (@app A (@firstn A j (@skipn A (S i) l)) (@cons A (@nth A i l d) (@skipn A (S (Init.Nat.add i j)) l))))) (@In A x (@app A (@firstn A i l) (@cons A (@nth A i l d) (@app A (@firstn A j (@skipn A (S i) l)) (@skipn A (S (Init.Nat.add i j)) l))))) *)
(* Goal: iff (@In A x (@app A (@firstn A i l) (@cons A (@nth A i l d) (@app A (@firstn A j (@skipn A (S i) l)) (@skipn A (S (Init.Nat.add i j)) l))))) (@In A x l) *)
split.
(* Goal: le i (@length A l) *)
intros [H | H]; subst; try omega.
(* Goal: and (le start x) (lt x (Init.Nat.add start (S len))) *)
(* Goal: forall _ : and (le start x) (lt x (Init.Nat.add start (S len))), or (@eq nat start x) (@In nat x (seq (S start) len)) *)
assert (S start <= x < S start + len).
(* Goal: @eq (list A) l l *)
rewrite <- IHlen; trivial.
(* Goal: le i (@length A l) *)
omega.
(* Goal: le i (@length A l) *)
intro H; rewrite IHlen; omega.
Qed.

Lemma nth_map_cst :
  forall {A B} (l:list A) n (d:B), nth n (map (fun _ => d) l) d = d.
Proof.
(* Goal: forall (A B : Type) (l : list A) (n : nat) (d : B), @eq B (@nth B n (@map A B (fun _ : A => d) l) d) d *)
intros A B l.
(* Goal: forall (a : A) (l : list A), @eq (list A) (@skipn A (Init.Nat.add (S i) j) (@cons A a l)) (@skipn A i (@skipn A j l)) *)
induction l as [ | a l IH]; intros [ | n] d; simpl; trivial.
Qed.

Lemma nth_S_tl A (l : list A) d n :
  nth n (tl l) d = nth (S n) l d.
Proof.
(* Goal: @eq (list A) l l *)
 intros; destruct l; simpl; intros; trivial.
(* Goal: @eq (list A) l l *)
 case n; trivial.
Qed.

Lemma map_ext2 : forall {A B} (f g : A -> B) l,
  (forall a : A, In a l -> f a = g a) -> map f l = map g l.
Proof.
(* Goal: forall (a : A) (l : list A), @eq (list A) (@skipn A (Init.Nat.add (S i) j) (@cons A a l)) (@skipn A i (@skipn A j l)) *)
 intros; induction l; simpl; trivial.
(* Goal: @eq (list A) (@skipn A (Init.Nat.add j (S i)) l) (@skipn A (S (Init.Nat.add i j)) l) *)
(* Goal: iff (@In A x (@app A (@firstn A i l) (@cons A (@nth A i l d) (@app A (@firstn A j (@skipn A (S i) l)) (@skipn A (S (Init.Nat.add i j)) l))))) (@In A x l) *)
 f_equal.
(* Goal: @eq B (f a) (g a) *)
(* Goal: @eq (list B) (@map A B f l) (@map A B g l) *)
 apply H; simpl; auto.
(* Goal: le (maxl l) e *)
 apply IHl.
(* Goal: @eq B (f a) (g a) *)
(* Goal: @eq (list B) (@map A B f l) (@map A B g l) *)
 intros; apply H; simpl; auto.
Qed.

Lemma map_nth2
  (A B : Type) (f : A -> B) (l : list A) b d n :
  (f d) = b ->
  nth n (map f l) b = f (nth n l d).
Proof. intros; rewrite <- H; apply map_nth. Qed.

Lemma length_plus_ex {A} n1 n2 (l : list A):
  length l = n1 + n2 ->
  exists l1, exists l2,
    length l1 = n1 /\ length l2 = n2 /\ l = l1 ++ l2.
Proof.
(* Goal: forall (A B : Type) (l : list A) (l2 : list B) (_ : @eq nat (@length B l2) (@length A l)), @eq (list A) (@firstn A (@length B l2) l) l *)
 intros.
(* Goal: @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => and (@eq nat (@length A l1) n1) (and (@eq nat (@length A l2) n2) (@eq (list A) l (@app A l1 l2))))) *)
 exists (firstn n1 l).
(* Goal: @ex (list A) (fun l2 : list A => and (@eq nat (@length A (@firstn A n1 l)) n1) (and (@eq nat (@length A l2) n2) (@eq (list A) l (@app A (@firstn A n1 l) l2)))) *)
 exists (skipn n1 l).
(* Goal: le i (@length A l) *)
 rewrite firstn_length, min_l, length_skipn, firstn_skipn; repeat split; omega.
Qed.

Lemma tl_app : forall A (l1 l2 : list A),
  l1 <> nil ->
  tl (l1 ++ l2) = tl l1 ++ l2.
Proof.
(* Goal: forall (a : A) (l : list A), @eq (list A) (@skipn A (Init.Nat.add (S i) j) (@cons A a l)) (@skipn A i (@skipn A j l)) *)
 intros; destruct l1; simpl; trivial.
(* Goal: @eq (list A) l l *)
 elim H; trivial.
Qed.

Lemma map_seq_nth : forall A B (l : list A) (g : A -> B) d, 
 map (fun n => g (nth n l d)) (seq 0 (length l)) = map g l.
Proof.
(* Goal: forall (A B : Type) (l : list A) (g : forall _ : A, B) (d : A), @eq (list B) (@map nat B (fun n : nat => g (@nth A n l d)) (seq O (@length A l))) (@map A B g l) *)
 intros A B l g d.
(* Goal: @eq (list B) (@map nat B (fun n : nat => g (@nth A n l d)) (seq O (@length A l))) (@map A B g l) *)
 change l with (skipn 0 l) at 3.
(* Goal: @eq (list B) (@map nat B (fun n : nat => g (@nth A n l d)) (seq O (@length A l))) (@map A B g (@skipn A O l)) *)
 rewrite <- map_nth_seq with (len := length l) (d := d).
(* Goal: @eq (list A) (@map nat A f (@map nat nat S (seq O m))) (@map nat A (fun x : nat => f (Init.Nat.sub x n)) (seq (S n) m)) *)
 rewrite map_map.
(* Goal: @eq nat (@length A l) (Init.Nat.add (@length A l) O) *)
 auto.
(* Goal: @eq nat (@length A l) (Init.Nat.add (@length A l) O) *)
 auto.
Qed.

Lemma map_seq_shift : forall A m (f : nat -> A) n,
n <> 0 ->
map f (seq 0 m) = map (fun x => f (x - n)%nat) (seq n m).
Proof.
(* Goal: @eq nat (@length A l) (Init.Nat.add (@length A l) O) *)
 induction m; simpl; intros; auto.
(* Goal: @eq (list A) (@skipn A (Init.Nat.add j (S i)) l) (@skipn A (S (Init.Nat.add i j)) l) *)
(* Goal: iff (@In A x (@app A (@firstn A i l) (@cons A (@nth A i l d) (@app A (@firstn A j (@skipn A (S i) l)) (@skipn A (S (Init.Nat.add i j)) l))))) (@In A x l) *)
 f_equal.
(* Goal: le i (@length A l) *)
 f_equal; omega.
(* Goal: @eq (list A) (@map nat A f (seq (S O) m)) (@map nat A (fun x : nat => f (Init.Nat.sub x n)) (seq (S n) m)) *)
 rewrite <- seq_shift with (start := 0).
(* Goal: @eq (list A) (@map nat A f (@map nat nat S (seq O m))) (@map nat A (fun x : nat => f (Init.Nat.sub x n)) (seq (S n) m)) *)
 rewrite map_map.
(* Goal: @eq (list A) (@map nat A (fun x : nat => f (S x)) (seq O m)) (@map nat A (fun x : nat => f (Init.Nat.sub x n)) (seq (S n) m)) *)
 rewrite IHm with (n := S n). 
(* Goal: @eq (list A) (@map nat A (fun x : nat => f (S (Init.Nat.sub x (S n)))) (seq (S n) m)) (@map nat A (fun x : nat => f (Init.Nat.sub x n)) (seq (S n) m)) *)
(* Goal: not (@eq nat (S n) O) *)
 apply map_ext2.
(* Goal: @eq (list A) (@skipn A (Init.Nat.add j (S i)) l) (@skipn A (S (Init.Nat.add i j)) l) *)
(* Goal: iff (@In A x (@app A (@firstn A i l) (@cons A (@nth A i l d) (@app A (@firstn A j (@skipn A (S i) l)) (@skipn A (S (Init.Nat.add i j)) l))))) (@In A x l) *)
 intros; f_equal.
(* Goal: @eq nat (S (Init.Nat.sub a (S n))) (Init.Nat.sub a n) *)
(* Goal: not (@eq nat (S n) O) *)
 rewrite in_seq_iff in H0.
(* Goal: le i (@length A l) *)
 omega.
(* Goal: le i (@length A l) *)
 omega.
Qed.

Lemma map_seq_nth_safe : forall A B (l : list A) (g : A -> B) d m, 
 map (fun n => g (nth (n - m) l d)) (seq m (length l)) = map g l.
Proof.
(* Goal: forall (A B : Type) (l : list A) (g : forall _ : A, B) (d : A) (m : nat), @eq (list B) (@map nat B (fun n : nat => g (@nth A (Init.Nat.sub n m) l d)) (seq m (@length A l))) (@map A B g l) *)
 intros A B l g d m.
(* Goal: @eq (list B) (@map nat B (fun n : nat => g (@nth A (Init.Nat.sub n m) l d)) (seq m (@length A l))) (@map A B g l) *)
 rewrite <- map_seq_nth with (d := d).
(* Goal: @eq (list B) (@map nat B (fun n : nat => g (@nth A (Init.Nat.sub n m) l d)) (seq m (@length A l))) (@map nat B (fun n : nat => g (@nth A n l d)) (seq O (@length A l))) *)
 destruct m; simpl.
(* Goal: forall (A B : Type) (l : list A) (l2 : list B) (_ : @eq nat (@length B l2) (@length A l)), @eq (list A) (@firstn A (@length B l2) l) l *)
 apply map_ext; intros.
(* Goal: @eq (list A) l l *)
 rewrite <- minus_n_O; trivial.
(* Goal: @eq nat (@length A l) (Init.Nat.add (@length A l) O) *)
 rewrite map_seq_shift with (n := S m); auto.
Qed.

Lemma seq_app : forall x y z,
  seq x y ++ seq (x + y) z = seq x (y + z).
Proof.
(* Goal: forall (A B : Type) (l : list A) (l2 : list B) (_ : @eq nat (@length B l2) (@length A l)), @eq (list A) (@firstn A (@length B l2) l) l *)
 intros.
(* Goal: @eq (list nat) (@app nat (seq x y) (seq (Init.Nat.add x y) z)) (seq x (Init.Nat.add y z)) *)
 rewrite <- firstn_skipn with (l := seq x (y + z)) (n := y).
(* Goal: @eq (list A) (@skipn A (Init.Nat.add j (S i)) l) (@skipn A (S (Init.Nat.add i j)) l) *)
(* Goal: iff (@In A x (@app A (@firstn A i l) (@cons A (@nth A i l d) (@app A (@firstn A j (@skipn A (S i) l)) (@skipn A (S (Init.Nat.add i j)) l))))) (@In A x l) *)
 f_equal.
(* Goal: @eq (list nat) (seq x y) (@firstn nat y (seq x (Init.Nat.add y z))) *)
(* Goal: @eq (list nat) (seq (Init.Nat.add x y) z) (@skipn nat y (seq x (Init.Nat.add y z))) *)
 rewrite firstn_seq.
(* Goal: @eq nat (@length A l) (Init.Nat.add (@length A l) O) *)
 rewrite Min.min_l; auto.
(* Goal: le i (@length A l) *)
 omega.
(* Goal: @eq (list nat) (seq (Init.Nat.add x y) z) (@skipn nat y (seq x (Init.Nat.add y z))) *)
 rewrite skipn_seq.
(* Goal: le i (@length A l) *)
 f_equal; omega.
Qed.

Definition andl {A} (P:A->Prop)(l:list A) : Prop :=
  fold_right (fun a res => P a /\ res) True l.

Lemma forall_andl A (P:A->Prop) l :
  (forall x, In x l -> P x) <-> andl P l.
Proof.
(* Goal: iff (forall (x : A) (_ : @In A x l), P x) (@andl A P l) *)
 induction l; simpl; intros;[ tauto | ].
(* Goal: iff (forall (x : A) (_ : or (@eq A a x) (@In A x l)), P x) (and (P a) (@andl A P l)) *)
 split; intro.
(* Goal: @eq nat (@length A l) (Init.Nat.add (@length A l) O) *)
 rewrite <- IHl; auto.
(* Goal: forall (x : A) (_ : or (@eq A a x) (@In A x l)), P x *)
 intros x [H1 | H2]; subst;[ tauto | ].
(* Goal: @eq nat (@length A l) (Init.Nat.add (@length A l) O) *)
 apply IHl; tauto.
Qed.

Fixpoint fun_power {A:Type}(n:nat)(f:A->A)(x:A) : A :=
  match n with
  | 0 => x
  | S n' => f (fun_power n' f x)
  end.

Lemma fun_power_minus_S : forall A (f:A->A) x m n,
  m < n -> f (fun_power (n - S m) f x) = fun_power (n - m) f x.
Proof.
(* Goal: forall (A : Type) (f : forall _ : A, A) (x : A) (m n : nat) (_ : lt m n), @eq A (f (@fun_power A (Init.Nat.sub n (S m)) f x)) (@fun_power A (Init.Nat.sub n m) f x) *)
 intros A f x m n H.
(* Goal: @eq (list A) l l *)
 replace (n-m) with (S (n - S m)) by omega; trivial.
Qed.

Definition mod2 (n : nat) : nat :=
  n - 2 * div2 n.

Fixpoint power (m n:nat) : nat :=
 match n with
 | 0 => 1
 | S n' => m * power m n'
 end.

Lemma power_le_l : forall a b n, a <= b -> power a n <= power b n.
Proof.
(* Goal: @eq (list A) l l *)
 induction n; simpl; intros; trivial.
(* Goal: @eq nat (@length A l) (Init.Nat.add (@length A l) O) *)
 apply mult_le_compat; tauto.
Qed.

Definition plusl (l:list nat) : nat :=
  fold_right plus 0 l.

Lemma plusl_cons : forall x l, plusl (x :: l) = x + plusl l.
Proof. trivial. Qed.

Lemma plusl_app l1 l2 :
  plusl (l1++l2) = plusl l1 + plusl l2.
Proof.
(* Goal: @eq (list A) l l *)
 induction l1; simpl; intros; trivial.
(* Goal: @eq nat (Init.Nat.mul a (multl (@app nat l1 l2))) (Init.Nat.mul (Init.Nat.mul a (multl l1)) (multl l2)) *)
 rewrite IHl1; ring.
Qed.

Lemma plusl_compat : forall A (l : list A) f g,
  (forall x, In x l -> f x <= g x) ->
  plusl (map f l) <= plusl (map g l).
Proof.
(* Goal: @eq nat (@length A l) (Init.Nat.add (@length A l) O) *)
 induction l; simpl; intros; auto.
(* Goal: @eq nat (@length A l) (Init.Nat.add (@length A l) O) *)
 apply plus_le_compat; auto.
Qed. 

Definition multl (l:list nat) : nat :=
  fold_right mult 1 l.

Lemma multl_app l1 l2 :
  multl (l1++l2) = multl l1 * multl l2.
Proof.
(* Goal: @eq (list A) l l *)
 induction l1; simpl; intros; trivial.
(* Goal: @eq nat (Init.Nat.mul a (multl (@app nat l1 l2))) (Init.Nat.mul (Init.Nat.mul a (multl l1)) (multl l2)) *)
 rewrite IHl1; ring.
Qed.

Lemma multl_plus_distr_l n l :
  n * plusl l = plusl (map (fun m => n * m) l).
Proof.
(* Goal: @eq nat (Init.Nat.mul n (plusl l)) (plusl (@map nat nat (fun m : nat => Init.Nat.mul n m) l)) *)
 induction l as [ | m l' IH]; simpl; intros; [ | rewrite <- IH]; ring.
Qed.

Fixpoint maxl l := 
  match l with
    | nil => 0
    | a :: l' => max a (maxl l')
  end.

Lemma in_le_maxl x l : In x l -> x <= maxl l.
Proof.
(* Goal: forall (A B : Type) (l : list A) (l2 : list B) (_ : @eq nat (@length B l2) (@length A l)), @eq (list A) (@firstn A (@length B l2) l) l *)
 induction l; simpl; intros.
(* Goal: @eq nat (@length A l) (Init.Nat.add (@length A l) O) *)
 tauto.
(* Goal: le x (Init.Nat.max a (maxl l)) *)
 destruct H; subst.
(* Goal: le n (Init.Nat.max n (Init.Nat.max n0 (maxl l))) *)
 apply Nat.le_max_l.
(* Goal: @eq nat (@length A l) (Init.Nat.add (@length A l) O) *)
 eapply le_trans; [ | apply Nat.le_max_r]; tauto.
Qed.

Lemma maxl_map A l (f : A -> nat) n :
  (forall x, In x l -> f x = n) ->
  maxl (map f l) <= n.
Proof.
(* Goal: @eq (list A) l l *)
 induction l; simpl; intros; trivial.
(* Goal: le i (@length A l) *)
 omega.
(* Goal: le (Init.Nat.max a (maxl l)) e *)
 apply Nat.max_lub.
(* Goal: @eq nat (@length A l) (Init.Nat.add (@length A l) O) *)
 rewrite H; auto.
(* Goal: le (maxl l) e *)
 apply IHl.
(* Goal: @eq nat (@length A l) (Init.Nat.add (@length A l) O) *)
 intros; apply H; auto.
Qed.

Lemma maxl_le l e :
  maxl l <= e ->
  (forall x, In x l -> x <= e).
Proof.
(* Goal: forall (_ : le (maxl l) e) (x : nat) (_ : @In nat x l), le x e *)
 induction l; simpl;[ tauto | intros].
(* Goal: le x e *)
 destruct H0; subst.
(* Goal: @eq (list A) l l *)
 apply Nat.max_lub_l with (maxl l); trivial.
(* Goal: @eq (list A) l l *)
 apply IHl; trivial.
(* Goal: @eq (list A) l l *)
 apply Nat.max_lub_r with a; trivial.
Qed.

Lemma maxl_eq_le l e :
  maxl l = e ->
  (forall x, In x l -> x <= e).
Proof.
(* Goal: forall (A B : Type) (l : list A) (l2 : list B) (_ : @eq nat (@length B l2) (@length A l)), @eq (list A) (@firstn A (@length B l2) l) l *)
 intros.
(* Goal: @eq nat (@length A l) (Init.Nat.add (@length A l) O) *)
 apply maxl_le with l; auto.
(* Goal: @eq nat (@length A l) (Init.Nat.add (@length A l) O) *)
 rewrite H; auto.
Qed.

Lemma maxl_eq_le3 e1 e2 e3 e :
  maxl [e1; e2; e3] = e ->
  e1 <= e /\ e2 <= e /\ e3 <= e.
Proof.
(* Goal: forall (A B : Type) (l : list A) (l2 : list B) (_ : @eq nat (@length B l2) (@length A l)), @eq (list A) (@firstn A (@length B l2) l) l *)
 intros.
(* Goal: and (le e1 e) (and (le e2 e) (le e3 e)) *)
 assert (Hl := maxl_eq_le _ _ H).
(* Goal: @eq nat (@length A l) (Init.Nat.add (@length A l) O) *)
 repeat split; apply Hl; simpl; auto.
Qed.

Lemma maxl_le3 e1 e2 e3 e :
  maxl [e1; e2; e3] <= e ->
  e1 <= e /\ e2 <= e /\ e3 <= e.
Proof.
(* Goal: forall (A B : Type) (l : list A) (l2 : list B) (_ : @eq nat (@length B l2) (@length A l)), @eq (list A) (@firstn A (@length B l2) l) l *)
 intros.
(* Goal: and (le e1 e) (and (le e2 e) (le e3 e)) *)
 assert (Hl := maxl_le _ _ H).
(* Goal: @eq nat (@length A l) (Init.Nat.add (@length A l) O) *)
 repeat split; apply Hl; simpl; auto.
Qed.

Lemma maxl_bound e1 e2 e3 e :
  e1 <= e -> e2 <= e -> e3 <= e ->
  maxl [e1; e2; e3] <= e.
Proof.
(* Goal: forall (A B : Type) (l : list A) (l2 : list B) (_ : @eq nat (@length B l2) (@length A l)), @eq (list A) (@firstn A (@length B l2) l) l *)
 intros.
(* Goal: @eq (list A) (@firstn A (S m) (@repeat A (S n) x)) (@repeat A (S m) x) *)
 simpl.
(* Goal: @eq (list A) l l *)
 apply Nat.max_lub; trivial.
(* Goal: @eq (list A) l l *)
 apply Nat.max_lub; trivial.
(* Goal: @eq (list A) l l *)
 apply Nat.max_lub; trivial.
(* Goal: le i (@length A l) *)
 omega.
Qed.

Lemma maxl_bound_in l e :
  (forall e', In e' l -> e' <= e) -> maxl l <= e.
Proof.
(* Goal: forall _ : forall (e' : nat) (_ : @In nat e' l), le e' e, le (maxl l) e *)
 induction l; simpl; intros;[ omega | ].
(* Goal: le (Init.Nat.max a (maxl l)) e *)
 apply Nat.max_lub.
(* Goal: @eq nat (@length A l) (Init.Nat.add (@length A l) O) *)
 apply H; auto.
(* Goal: le (maxl l) e *)
 apply IHl.
(* Goal: @eq nat (@length A l) (Init.Nat.add (@length A l) O) *)
 intros; apply H; auto.
Qed.

Lemma maxl_cons l n : n <= maxl (n :: l).
Proof.
(* Goal: forall (A B : Type) (l : list A) (l2 : list B) (_ : @eq nat (@length B l2) (@length A l)), @eq (list A) (@firstn A (@length B l2) l) l *)
 destruct l; simpl; intros.
(* Goal: le n (Init.Nat.max n O) *)
(* Goal: le n (Init.Nat.max n (Init.Nat.max n0 (maxl l))) *)
 auto with arith.
(* Goal: le n (Init.Nat.max n (Init.Nat.max n0 (maxl l))) *)
 apply Nat.le_max_l.
Qed.

Lemma le_maxl_cons l m n :
 n <= maxl l -> n <= maxl (m :: l).
Proof.
(* Goal: forall _ : forall (e' : nat) (_ : @In nat e' l), le e' e, le (maxl l) e *)
 induction l; simpl; intros;[ omega | ].
 eapply le_trans.
 apply Nat.le_max_r.
(* Goal: @eq (list A) l l *)
 apply Nat.max_le_compat_l; trivial.
Qed.

Lemma nth_maxl_bound : forall A (l : list A) (m:A->nat) d i,
  m d = 0 -> m (nth i l d) <= maxl (map m l).
Proof.
intros A l m d.
(* Goal: @eq (list A) (@firstn A (S m) (@repeat A (S n) x)) (@repeat A (S m) x) *)
induction l as [ | a l IH]; intros [ | i] H; simpl.
(* Goal: le i (@length A l) *)
omega.
(* Goal: le i (@length A l) *)
omega.
(* Goal: le n (Init.Nat.max n O) *)
(* Goal: le n (Init.Nat.max n (Init.Nat.max n0 (maxl l))) *)
auto with arith.
eapply le_trans.
(* Goal: @eq (list A) (@firstn A m (@repeat A n x)) (@repeat A m x) *)
apply IH.
exact H.
apply Nat.le_max_r.
Qed.

Lemma length_hd_app A (l1 l2 : list (list A)) :
  length (hd nil l1) <= length (hd nil (l1 ++ l2)).
Proof. intros; case l1; simpl; trivial; omega. Qed.

Lemma length_nth_app A (l1 l2 : list (list A)) i :
  length (nth i l1 nil) <= length (nth i (l1 ++ l2) nil).
Proof.
(* Goal: le (@length A (@nth (list A) i l1 (@nil A))) (@length A (@nth (list A) i (@app (list A) l1 l2) (@nil A))) *)
 intros; destruct (le_lt_dec (length l1) i).
(* Goal: le i (@length A l) *)
 rewrite nth_overflow; simpl; trivial; omega.
(* Goal: @eq (list A) l l *)
 rewrite app_nth1; trivial.
Qed.

Lemma maxl_nth l :
  exists i, maxl l = nth i l 0.
Proof.
(* Goal: @eq (list A) (@firstn A (S m) (@repeat A (S n) x)) (@repeat A (S m) x) *)
 induction l; simpl.
(* Goal: @eq (list A) l l *)
 exists 0; trivial.
(* Goal: @ex nat (fun i : nat => @eq nat (Init.Nat.max a (maxl l)) match i with | O => a | S m => @nth nat m l O end) *)
 destruct IHl.
(* Goal: @ex nat (fun i : nat => @eq nat (Init.Nat.max a (maxl l)) match i with | O => a | S m => @nth nat m l O end) *)
 destruct (le_lt_dec a (maxl l)).
(* Goal: @eq (list A) l l *)
 rewrite max_r; trivial.
(* Goal: @eq (list A) l l *)
 exists (S x); trivial.
(* Goal: @eq (list A) l l *)
 exists 0; rewrite max_l; trivial.
(* Goal: le i (@length A l) *)
 omega.
Qed.

Lemma maxl_map_0 A l (f : A -> nat)  :
  (forall x, In x l -> (f x) = 0) ->
  maxl (map f l) = 0.
Proof.
(* Goal: @eq (list A) l l *)
 induction l; simpl; intros; trivial.
(* Goal: @eq nat (@length A l) (Init.Nat.add (@length A l) O) *)
 rewrite H, IHl; simpl; trivial; intros; auto.
Qed.

Lemma maxl_le_plusl : forall l, maxl l <= plusl l.
Proof.
(* Goal: @eq (list A) (@firstn A (S m) (@repeat A (S n) x)) (@repeat A (S m) x) *)
 induction l; trivial; simpl.
(* Goal: le i (@length A l) *)
 apply Nat.max_lub; omega.
Qed.

Lemma forallb_forall_conv :
  forall A f (l:list A), forallb f l = false <-> (exists x, In x l /\ f x = false).
Proof.
(* Goal: iff (@In A x (@app A (@firstn A i l) (@app A (@firstn A j (@skipn A (S i) l)) (@cons A (@nth A i l d) (@skipn A (S (Init.Nat.add i j)) l))))) (@In A x (@app A (@firstn A i l) (@cons A (@nth A i l d) (@app A (@firstn A j (@skipn A (S i) l)) (@skipn A (S (Init.Nat.add i j)) l))))) *)
(* Goal: iff (@In A x (@app A (@firstn A i l) (@cons A (@nth A i l d) (@app A (@firstn A j (@skipn A (S i) l)) (@skipn A (S (Init.Nat.add i j)) l))))) (@In A x l) *)
 induction l as [ | x l IH]; simpl; split.
(* Goal: @eq A x y *)
(* Goal: @eq A x y *)
 congruence.
(* Goal: @eq nat (@length A l) (Init.Nat.add (@length A l) O) *)
 intros [x H]; tauto.
(* Goal: forall _ : @eq bool (andb (f x) (@forallb A f l)) false, @ex A (fun x0 : A => and (or (@eq A x x0) (@In A x0 l)) (@eq bool (f x0) false)) *)
(* Goal: forall _ : @ex A (fun x0 : A => and (or (@eq A x x0) (@In A x0 l)) (@eq bool (f x0) false)), @eq bool (andb (f x) (@forallb A f l)) false *)
 intro H.
(* Goal: @ex A (fun x0 : A => and (or (@eq A x x0) (@In A x0 l)) (@eq bool (f x0) false)) *)
(* Goal: forall _ : @ex A (fun x0 : A => and (or (@eq A x x0) (@In A x0 l)) (@eq bool (f x0) false)), @eq bool (andb (f x) (@forallb A f l)) false *)
 apply andb_false_elim in H.
(* Goal: @eq A x y *)
 destruct H as [H | H].
(* Goal: @eq nat (@length A l) (Init.Nat.add (@length A l) O) *)
 exists x; tauto.
(* Goal: @ex A (fun x0 : A => and (or (@eq A x x0) (@In A x0 l)) (@eq bool (f x0) false)) *)
(* Goal: forall _ : @ex A (fun x0 : A => and (or (@eq A x x0) (@In A x0 l)) (@eq bool (f x0) false)), @eq bool (andb (f x) (@forallb A f l)) false *)
 rewrite IH in H.
(* Goal: @eq nat (@length A l) (Init.Nat.add (@length A l) O) *)
 destruct H as [y H]; exists y; tauto.
(* Goal: forall _ : @ex A (fun x0 : A => and (or (@eq A x x0) (@In A x0 l)) (@eq bool (f x0) false)), @eq bool (andb (f x) (@forallb A f l)) false *)
 intros [y H].
(* Goal: @eq bool (andb (f x) (@forallb A f l)) false *)
 apply andb_false_iff.
(* Goal: @eq nat (@length A l) (Init.Nat.add (@length A l) O) *)
 destruct H as [ [H1 | H1] H2]; subst; auto.
(* Goal: @eq nat (@length A l) (Init.Nat.add (@length A l) O) *)
 right; rewrite IH; exists y; tauto.
Qed.

Lemma forallb_nth : forall A (l : list A) (p : A -> bool) n d,
  p d = true ->
  forallb p l = true ->
  p (nth n l d) = true.
Proof.
 induction l; simpl; intros; case n; trivial; intros;
(* Goal: @eq nat (@length A l) (Init.Nat.add (@length A l) O) *)
   rewrite andb_true_iff in H0; [ | apply IHl ]; tauto.
Qed.

Lemma forallb_hd : forall A (l : list A) (p : A -> bool) d,
  forallb p l = true ->
  p d = true ->
  p (hd d l) = true.
Proof.
(* Goal: @eq (list A) l l *)
 destruct l; simpl; intros; trivial.
(* Goal: @eq nat (@length A l) (Init.Nat.add (@length A l) O) *)
 rewrite andb_true_iff in H; tauto.
Qed.

Lemma forallb_tl : forall A (l : list A) (p : A -> bool),
  forallb p l = true ->
  forallb p (tail l) = true.
Proof.
(* Goal: @eq (list A) l l *)
 induction l; simpl; intros; trivial.
(* Goal: @eq nat (@length A l) (Init.Nat.add (@length A l) O) *)
 rewrite andb_true_iff in H; tauto.
Qed.

Lemma forallb_map : forall A B (l : list A) (p : B -> bool) (f : A -> B),
  (forall x, In x l -> p (f x) = true) ->
  forallb p (map f l) = true.
Proof.
(* Goal: forall (A B : Type) (l : list A) (p : forall _ : B, bool) (f : forall _ : A, B) (_ : forall (x : A) (_ : @In A x l), @eq bool (p (f x)) true), @eq bool (@forallb B p (@map A B f l)) true *)
 intros; apply forallb_forall.
(* Goal: forall (A B : Type) (l : list A) (l2 : list B) (_ : @eq nat (@length B l2) (@length A l)), @eq (list A) (@firstn A (@length B l2) l) l *)
 intros.
(* Goal: @eq bool (p x) true *)
 apply in_map_iff in H0.
(* Goal: @eq nat (@length A l) (Init.Nat.add (@length A l) O) *)
 destruct H0 as ( x' & H0 & H1); subst; auto.
Qed.

Fixpoint repeat {A:Type}(n:nat)(x:A) : list A :=
  match n with
  | 0 => nil
  | S n' => x :: repeat n' x
  end.

Lemma firstn_repeat_le :
  forall A (x:A) m n,
  m <= n ->
  firstn m (repeat n x) = repeat m x.
Proof.
(* Goal: forall (A : Type) (x : A) (m n : nat) (_ : le m n), @eq (list A) (@firstn A m (@repeat A n x)) (@repeat A m x) *)
intros A x m.
(* Goal: forall (n : nat) (_ : le m n), @eq (list A) (@firstn A m (@repeat A n x)) (@repeat A m x) *)
induction m as [ | m IH]; intros n H.
(* Goal: @eq (list A) l l *)
trivial.
(* Goal: @eq (list A) (@firstn A (S m) (@repeat A n x)) (@repeat A (S m) x) *)
destruct n as [ | n].
(* Goal: @eq A match i with | O => d | S m => d end x *)
(* Goal: @eq A match i with | O => x | S m => @nth A m (@repeat A n x) d end x *)
contradict H.
(* Goal: le i (@length A l) *)
omega.
(* Goal: @eq (list A) (@firstn A (S m) (@repeat A (S n) x)) (@repeat A (S m) x) *)
simpl.
(* Goal: @eq (list A) (@skipn A (Init.Nat.add j (S i)) l) (@skipn A (S (Init.Nat.add i j)) l) *)
(* Goal: iff (@In A x (@app A (@firstn A i l) (@cons A (@nth A i l d) (@app A (@firstn A j (@skipn A (S i) l)) (@skipn A (S (Init.Nat.add i j)) l))))) (@In A x l) *)
f_equal.
(* Goal: @eq (list A) (@firstn A m (@repeat A n x)) (@repeat A m x) *)
apply IH.
(* Goal: le i (@length A l) *)
omega.
Qed.

Lemma in_repeat_eq : forall A (x y:A) n, In x (repeat n y) -> x=y.
Proof.
(* Goal: forall (A : Type) (x y : A) (n : nat) (_ : @In A x (@repeat A n y)), @eq A x y *)
 induction n as [ | n IH]; simpl; intro H; [ tauto | ].
(* Goal: @eq A x y *)
 destruct H as [H | H].
(* Goal: @eq A x y *)
(* Goal: @eq A x y *)
 congruence.
(* Goal: @eq nat (@length A l) (Init.Nat.add (@length A l) O) *)
 tauto.
Qed.

Lemma map_repeat : forall A B (f:A->B) n x, map f (repeat n x) = repeat n (f x).
Proof.
(* Goal: forall (A B : Type) (f : forall _ : A, B) (n : nat) (x : A), @eq (list B) (@map A B f (@repeat A n x)) (@repeat B n (f x)) *)
 induction n as [ | n IH].
(* Goal: @eq (list A) l l *)
 trivial.
(* Goal: @eq A x y *)
(* Goal: @eq A x y *)
 simpl; congruence.
Qed.

Lemma multl_repeat_power : forall n x, multl (repeat n x) = power x n.
Proof. induction n as [ | n IH]; trivial; simpl; congruence. Qed.

Lemma length_repeat : forall A n (x:A), length (repeat n x) = n.
Proof. induction n; simpl; intros; trivial; congruence. Qed.

Lemma nth_repeat :
  forall A n (x:A) d i, i < n ->
  nth i (repeat n x) d = x.
Proof.
(* Goal: forall (A : Type) (n : nat) (x d : A) (i : nat) (_ : lt i n), @eq A (@nth A i (@repeat A n x) d) x *)
 intros A n x d.
(* Goal: forall (i : nat) (_ : lt i n), @eq A (@nth A i (@repeat A n x) d) x *)
 induction n as [ | n IH]; simpl ; intros i H.
(* Goal: @eq A match i with | O => d | S m => d end x *)
(* Goal: @eq A match i with | O => x | S m => @nth A m (@repeat A n x) d end x *)
 contradict H.
(* Goal: le i (@length A l) *)
 omega.
(* Goal: le n (Init.Nat.max n O) *)
(* Goal: le n (Init.Nat.max n (Init.Nat.max n0 (maxl l))) *)
 destruct i as [ | i]; auto with arith.
Qed.

Definition move_forward {A}(i j:nat)(l:list A)(d:A) : list A :=
  firstn i l ++ firstn j (skipn (S i) l) ++ (nth i l d :: skipn (S (i+j)) l).

Lemma move_forward_map A B d1 d2 i j (f:A->B) l :
  f d1 = d2 ->
  move_forward i j (map f l) d2 = map f (move_forward i j l d1).
Proof.
(* Goal: forall _ : @eq B (f d1) d2, @eq (list B) (@move_forward B i j (@map A B f l) d2) (@map A B f (@move_forward A i j l d1)) *)
 intros; unfold move_forward.
(* Goal: @eq (list A) (@skipn A (Init.Nat.add j (S i)) l) (@skipn A (S (Init.Nat.add i j)) l) *)
(* Goal: iff (@In A x (@app A (@firstn A i l) (@cons A (@nth A i l d) (@app A (@firstn A j (@skipn A (S i) l)) (@skipn A (S (Init.Nat.add i j)) l))))) (@In A x l) *)
 rewrite !map_app; f_equal.
(* Goal: @eq (list A) l l *)
 rewrite map_firstn; trivial.
(* Goal: @eq (list A) (@skipn A (Init.Nat.add j (S i)) l) (@skipn A (S (Init.Nat.add i j)) l) *)
(* Goal: iff (@In A x (@app A (@firstn A i l) (@cons A (@nth A i l d) (@app A (@firstn A j (@skipn A (S i) l)) (@skipn A (S (Init.Nat.add i j)) l))))) (@In A x l) *)
 f_equal.
(* Goal: @eq (list A) l l *)
 rewrite map_firstn, map_skipn; trivial.
(* Goal: @eq (list A) l l *)
 rewrite map_nth2 with (d:=d1); trivial.
(* Goal: @eq (list A) l l *)
 rewrite <- map_skipn; trivial.
Qed.

Lemma length_move_forward :
  forall A i j (l:list A) d, i+j < length l -> length (move_forward i j l d) = length l.
Proof.
(* Goal: forall (A : Type) (x : A) (i j : nat) (d : A) (l : list A) (_ : lt i (@length A l)), iff (@In A x (@move_forward A i j l d)) (@In A x l) *)
unfold move_forward.
(* Goal: forall (A B : Type) (l : list A) (l2 : list B) (_ : @eq nat (@length B l2) (@length A l)), @eq (list A) (@firstn A (@length B l2) l) l *)
intros.
(* Goal: @eq nat (@length A (@app A (@firstn A i l) (@app A (@firstn A j (@skipn A (S i) l)) (@cons A (@nth A i l d) (@skipn A (S (Init.Nat.add i j)) l))))) (@length A l) *)
do 2 rewrite app_length.
(* Goal: @eq nat (Init.Nat.add (@length A (@firstn A i l)) (Init.Nat.add (@length A (@firstn A j (@skipn A (S i) l))) (@length A (@cons A (@nth A i l d) (@skipn A (S (Init.Nat.add i j)) l))))) (@length A l) *)
do 2 rewrite firstn_length.
(* Goal: @eq nat (Init.Nat.add i (Init.Nat.add (Init.Nat.min j (@length A (@skipn A (S i) l))) (@length A (@cons A (@nth A i l d) (@skipn A (S (Init.Nat.add i j)) l))))) (@length A l) *)
(* Goal: le i (@length A l) *)
rewrite min_l.
(* Goal: @eq nat (Init.Nat.add i (Init.Nat.add (Init.Nat.min j (@length A (@skipn A (S i) l))) (@length A (@cons A (@nth A i l d) (@skipn A (S (Init.Nat.add i j)) l))))) (@length A l) *)
(* Goal: le i (@length A l) *)
rewrite min_l.
(* Goal: @eq nat (Init.Nat.add i (Init.Nat.add j (@length A (@cons A (@nth A i l d) (@skipn A (S (Init.Nat.add i j)) l))))) (@length A l) *)
(* Goal: le j (@length A (@skipn A (S i) l)) *)
(* Goal: le i (@length A l) *)
change (length (nth i l d :: skipn (S (i + j)) l)) with (1 + length (skipn (S (i + j)) l)).
(* Goal: le j (@length A (@skipn A (S i) l)) *)
(* Goal: le i (@length A l) *)
rewrite length_skipn.
(* Goal: le i (@length A l) *)
omega.
(* Goal: le j (@length A (@skipn A (S i) l)) *)
(* Goal: le i (@length A l) *)
rewrite length_skipn.
(* Goal: le i (@length A l) *)
omega.
(* Goal: le i (@length A l) *)
omega.
Qed.

Lemma in_move_forward_iff :
  forall A x i j d (l:list A), i < length l -> (In x (move_forward i j l d) <-> In x l).
Proof.
(* Goal: forall (A : Type) (x : A) (i j : nat) (d : A) (l : list A) (_ : lt i (@length A l)), iff (@In A x (@move_forward A i j l d)) (@In A x l) *)
unfold move_forward.
(* Goal: forall (A : Type) (x : A) (i j : nat) (d : A) (l : list A) (_ : lt i (@length A l)), iff (@In A x (@app A (@firstn A i l) (@app A (@firstn A j (@skipn A (S i) l)) (@cons A (@nth A i l d) (@skipn A (S (Init.Nat.add i j)) l))))) (@In A x l) *)
intros A x i j d l Hi.
(* Goal: iff (@In A x (@app A (@firstn A i l) (@app A (@firstn A j (@skipn A (S i) l)) (@cons A (@nth A i l d) (@skipn A (S (Init.Nat.add i j)) l))))) (@In A x l) *)
transitivity (In x (firstn i l ++ nth i l d :: firstn j (skipn (S i) l) ++ skipn (S (i + j)) l)).
(* Goal: iff (@In A x (@app A (@firstn A i l) (@app A (@firstn A j (@skipn A (S i) l)) (@cons A (@nth A i l d) (@skipn A (S (Init.Nat.add i j)) l))))) (@In A x (@app A (@firstn A i l) (@cons A (@nth A i l d) (@app A (@firstn A j (@skipn A (S i) l)) (@skipn A (S (Init.Nat.add i j)) l))))) *)
(* Goal: iff (@In A x (@app A (@firstn A i l) (@cons A (@nth A i l d) (@app A (@firstn A j (@skipn A (S i) l)) (@skipn A (S (Init.Nat.add i j)) l))))) (@In A x l) *)
split.
(* Goal: forall _ : @In A x (@app A (@firstn A i l) (@cons A (@nth A i l d) (@app A (@firstn A j (@skipn A (S i) l)) (@skipn A (S (Init.Nat.add i j)) l)))), @In A x (@app A (@firstn A i l) (@app A (@firstn A j (@skipn A (S i) l)) (@cons A (@nth A i l d) (@skipn A (S (Init.Nat.add i j)) l)))) *)
(* Goal: iff (@In A x (@app A (@firstn A i l) (@cons A (@nth A i l d) (@app A (@firstn A j (@skipn A (S i) l)) (@skipn A (S (Init.Nat.add i j)) l))))) (@In A x l) *)
apply Permutation_in.
(* Goal: @Permutation A (@app A (@firstn A i l) (@cons A (@nth A i l d) (@app A (@firstn A j (@skipn A (S i) l)) (@skipn A (S (Init.Nat.add i j)) l)))) (@app A (@firstn A i l) (@app A (@firstn A j (@skipn A (S i) l)) (@cons A (@nth A i l d) (@skipn A (S (Init.Nat.add i j)) l)))) *)
(* Goal: iff (@In A x (@app A (@firstn A i l) (@cons A (@nth A i l d) (@app A (@firstn A j (@skipn A (S i) l)) (@skipn A (S (Init.Nat.add i j)) l))))) (@In A x l) *)
apply Permutation_app_head.
(* Goal: @Permutation A (@app A (@firstn A j (@skipn A (S i) l)) (@cons A (@nth A i l d) (@skipn A (S (Init.Nat.add i j)) l))) (@cons A (@nth A i l d) (@app A (@firstn A j (@skipn A (S i) l)) (@skipn A (S (Init.Nat.add i j)) l))) *)
(* Goal: forall _ : @In A x (@app A (@firstn A i l) (@cons A (@nth A i l d) (@app A (@firstn A j (@skipn A (S i) l)) (@skipn A (S (Init.Nat.add i j)) l)))), @In A x (@app A (@firstn A i l) (@app A (@firstn A j (@skipn A (S i) l)) (@cons A (@nth A i l d) (@skipn A (S (Init.Nat.add i j)) l)))) *)
(* Goal: iff (@In A x (@app A (@firstn A i l) (@cons A (@nth A i l d) (@app A (@firstn A j (@skipn A (S i) l)) (@skipn A (S (Init.Nat.add i j)) l))))) (@In A x l) *)
apply Permutation_sym.
(* Goal: @Permutation A (@cons A (@nth A i l d) (@app A (@firstn A j (@skipn A (S i) l)) (@skipn A (S (Init.Nat.add i j)) l))) (@app A (@firstn A j (@skipn A (S i) l)) (@cons A (@nth A i l d) (@skipn A (S (Init.Nat.add i j)) l))) *)
(* Goal: iff (@In A x (@app A (@firstn A i l) (@cons A (@nth A i l d) (@app A (@firstn A j (@skipn A (S i) l)) (@skipn A (S (Init.Nat.add i j)) l))))) (@In A x l) *)
apply Permutation_middle.
(* Goal: forall _ : @In A x (@app A (@firstn A i l) (@cons A (@nth A i l d) (@app A (@firstn A j (@skipn A (S i) l)) (@skipn A (S (Init.Nat.add i j)) l)))), @In A x (@app A (@firstn A i l) (@app A (@firstn A j (@skipn A (S i) l)) (@cons A (@nth A i l d) (@skipn A (S (Init.Nat.add i j)) l)))) *)
(* Goal: iff (@In A x (@app A (@firstn A i l) (@cons A (@nth A i l d) (@app A (@firstn A j (@skipn A (S i) l)) (@skipn A (S (Init.Nat.add i j)) l))))) (@In A x l) *)
apply Permutation_in.
(* Goal: @Permutation A (@app A (@firstn A i l) (@cons A (@nth A i l d) (@app A (@firstn A j (@skipn A (S i) l)) (@skipn A (S (Init.Nat.add i j)) l)))) (@app A (@firstn A i l) (@app A (@firstn A j (@skipn A (S i) l)) (@cons A (@nth A i l d) (@skipn A (S (Init.Nat.add i j)) l)))) *)
(* Goal: iff (@In A x (@app A (@firstn A i l) (@cons A (@nth A i l d) (@app A (@firstn A j (@skipn A (S i) l)) (@skipn A (S (Init.Nat.add i j)) l))))) (@In A x l) *)
apply Permutation_app_head.
(* Goal: @Permutation A (@cons A (@nth A i l d) (@app A (@firstn A j (@skipn A (S i) l)) (@skipn A (S (Init.Nat.add i j)) l))) (@app A (@firstn A j (@skipn A (S i) l)) (@cons A (@nth A i l d) (@skipn A (S (Init.Nat.add i j)) l))) *)
(* Goal: iff (@In A x (@app A (@firstn A i l) (@cons A (@nth A i l d) (@app A (@firstn A j (@skipn A (S i) l)) (@skipn A (S (Init.Nat.add i j)) l))))) (@In A x l) *)
apply Permutation_middle.
(* Goal: iff (@In A x (@app A (@firstn A i l) (@cons A (@nth A i l d) (@app A (@firstn A j (@skipn A (S i) l)) (@skipn A (S (Init.Nat.add i j)) l))))) (@In A x l) *)
assert (l = firstn i l ++ nth i l d :: firstn j (skipn (S i) l) ++ skipn (S (i + j)) l) as H.
(* Goal: @eq (list A) l (@app A (@firstn A i l) (@cons A (@nth A i l d) (@app A (@firstn A j (@skipn A (S i) l)) (@skipn A (S (Init.Nat.add i j)) l)))) *)
(* Goal: iff (@In A x (@app A (@firstn A i l) (@cons A (@nth A i l d) (@app A (@firstn A j (@skipn A (S i) l)) (@skipn A (S (Init.Nat.add i j)) l))))) (@In A x l) *)
rewrite <- (firstn_skipn i l) at 1.
(* Goal: @eq (list A) (@skipn A (Init.Nat.add j (S i)) l) (@skipn A (S (Init.Nat.add i j)) l) *)
(* Goal: iff (@In A x (@app A (@firstn A i l) (@cons A (@nth A i l d) (@app A (@firstn A j (@skipn A (S i) l)) (@skipn A (S (Init.Nat.add i j)) l))))) (@In A x l) *)
f_equal.
(* Goal: @eq (list A) (@skipn A i l) (@cons A (@nth A i l d) (@app A (@firstn A j (@skipn A (S i) l)) (@skipn A (S (Init.Nat.add i j)) l))) *)
(* Goal: iff (@In A x (@app A (@firstn A i l) (@cons A (@nth A i l d) (@app A (@firstn A j (@skipn A (S i) l)) (@skipn A (S (Init.Nat.add i j)) l))))) (@In A x l) *)
transitivity (nth i l d :: skipn (S i) l).
(* Goal: @eq (list A) (@skipn A i l) (@cons A (@nth A i l d) (@skipn A (S i) l)) *)
(* Goal: @eq (list A) (@cons A (@nth A i l d) (@skipn A (S i) l)) (@cons A (@nth A i l d) (@app A (@firstn A j (@skipn A (S i) l)) (@skipn A (S (Init.Nat.add i j)) l))) *)
(* Goal: iff (@In A x (@app A (@firstn A i l) (@cons A (@nth A i l d) (@app A (@firstn A j (@skipn A (S i) l)) (@skipn A (S (Init.Nat.add i j)) l))))) (@In A x l) *)
symmetry.
(* Goal: @eq (list A) (@cons A (@nth A i l d) (@skipn A (S i) l)) (@skipn A i l) *)
(* Goal: @eq (list A) (@cons A (@nth A i l d) (@skipn A (S i) l)) (@cons A (@nth A i l d) (@app A (@firstn A j (@skipn A (S i) l)) (@skipn A (S (Init.Nat.add i j)) l))) *)
(* Goal: iff (@In A x (@app A (@firstn A i l) (@cons A (@nth A i l d) (@app A (@firstn A j (@skipn A (S i) l)) (@skipn A (S (Init.Nat.add i j)) l))))) (@In A x l) *)
apply cons_skipn.
(* Goal: @eq (list A) l l *)
trivial.
(* Goal: @eq (list A) (@skipn A (Init.Nat.add j (S i)) l) (@skipn A (S (Init.Nat.add i j)) l) *)
(* Goal: iff (@In A x (@app A (@firstn A i l) (@cons A (@nth A i l d) (@app A (@firstn A j (@skipn A (S i) l)) (@skipn A (S (Init.Nat.add i j)) l))))) (@In A x l) *)
f_equal.
(* Goal: @eq (list A) (@skipn A (S i) l) (@app A (@firstn A j (@skipn A (S i) l)) (@skipn A (S (Init.Nat.add i j)) l)) *)
(* Goal: iff (@In A x (@app A (@firstn A i l) (@cons A (@nth A i l d) (@app A (@firstn A j (@skipn A (S i) l)) (@skipn A (S (Init.Nat.add i j)) l))))) (@In A x l) *)
transitivity (firstn j (skipn (S i) l) ++ skipn j (skipn (S i) l)).
(* Goal: @eq (list A) (@skipn A (S i) l) (@app A (@firstn A j (@skipn A (S i) l)) (@skipn A j (@skipn A (S i) l))) *)
(* Goal: @eq (list A) (@app A (@firstn A j (@skipn A (S i) l)) (@skipn A j (@skipn A (S i) l))) (@app A (@firstn A j (@skipn A (S i) l)) (@skipn A (S (Init.Nat.add i j)) l)) *)
(* Goal: iff (@In A x (@app A (@firstn A i l) (@cons A (@nth A i l d) (@app A (@firstn A j (@skipn A (S i) l)) (@skipn A (S (Init.Nat.add i j)) l))))) (@In A x l) *)
rewrite firstn_skipn.
(* Goal: @eq (list A) l l *)
trivial.
(* Goal: @eq (list A) (@skipn A (Init.Nat.add j (S i)) l) (@skipn A (S (Init.Nat.add i j)) l) *)
(* Goal: iff (@In A x (@app A (@firstn A i l) (@cons A (@nth A i l d) (@app A (@firstn A j (@skipn A (S i) l)) (@skipn A (S (Init.Nat.add i j)) l))))) (@In A x l) *)
f_equal.
(* Goal: @eq (list A) (@skipn A j (@skipn A (S i) l)) (@skipn A (S (Init.Nat.add i j)) l) *)
(* Goal: iff (@In A x (@app A (@firstn A i l) (@cons A (@nth A i l d) (@app A (@firstn A j (@skipn A (S i) l)) (@skipn A (S (Init.Nat.add i j)) l))))) (@In A x l) *)
rewrite <- skipn_plus.
(* Goal: @eq (list A) (@skipn A (Init.Nat.add j (S i)) l) (@skipn A (S (Init.Nat.add i j)) l) *)
(* Goal: iff (@In A x (@app A (@firstn A i l) (@cons A (@nth A i l d) (@app A (@firstn A j (@skipn A (S i) l)) (@skipn A (S (Init.Nat.add i j)) l))))) (@In A x l) *)
f_equal.
(* Goal: @eq nat (Init.Nat.add j (S i)) (S (Init.Nat.add i j)) *)
(* Goal: iff (@In A x (@app A (@firstn A i l) (@cons A (@nth A i l d) (@app A (@firstn A j (@skipn A (S i) l)) (@skipn A (S (Init.Nat.add i j)) l))))) (@In A x l) *)
ring.
(* Goal: iff (@In A x (@app A (@firstn A i l) (@cons A (@nth A i l d) (@app A (@firstn A j (@skipn A (S i) l)) (@skipn A (S (Init.Nat.add i j)) l))))) (@In A x l) *)
rewrite H at 5.
(* Goal: @eq nat (@length A l) (Init.Nat.add (@length A l) O) *)
tauto.
Qed.

Lemma firstn_simpl : forall A B (l : list A) (l2 : list B),
 length l2 = length l ->
 firstn (length l2) l = l.
Proof.
(* Goal: forall (A B : Type) (l : list A) (l2 : list B) (_ : @eq nat (@length B l2) (@length A l)), @eq (list A) (@firstn A (@length B l2) l) l *)
 intros.
(* Goal: @eq (list A) (@firstn A (@length B l2) l) l *)
 rewrite H.
(* Goal: @eq (list A) (@firstn A (@length A l) l) l *)
 rewrite <- app_nil_r with (l := l) at 2 .
(* Goal: @eq (list A) (@firstn A (@length A l) (@app A l (@nil A))) l *)
 rewrite firstn_app.
(* Goal: @eq (list A) l l *)
 trivial.
Qed.

Lemma firstn_app2 : forall (A : Type) (l l' : list A) n, 
 length l = n -> firstn n (l ++ l') = l .
Proof. intros; subst; apply firstn_app. Qed.

Lemma firstn_firstn : forall A n (l : list A),
 firstn n (firstn n l) = firstn n l.
Proof.
(* Goal: @eq nat (@length A l) (Init.Nat.add (@length A l) O) *)
 induction n; simpl; auto.
(* Goal: @eq nat (@length A l) (Init.Nat.add (@length A l) O) *)
 intros [ | a l]; try rewrite IHn; auto.
Qed.

Lemma In_firstn : forall A n a (l : list A),
  In a (firstn n l) -> In a l.
Proof.
(* Goal: forall (A : Type) (n : nat) (y : list A) (d : A) (_ : lt n (@length A y)), @eq (list A) (@skipn A n y) (@cons A (@nth A n y d) (@skipn A (S n) y)) *)
 intros A; induction n; simpl; intros.
(* Goal: False *)
(* Goal: or (@eq A a0 a) (@In A a l) *)
 elim H.
(* Goal: @In A a l *)
 destruct l; simpl in *.
(* Goal: False *)
(* Goal: or (@eq A a0 a) (@In A a l) *)
 elim H.
(* Goal: @eq nat (@length A l) (Init.Nat.add (@length A l) O) *)
 destruct H; subst; auto.
Qed.
