Require Import List.
Require Import Arith.
Fixpoint nth_option (A:Set)(n:nat)(l:list A) {struct l}
: option A :=
match n, l with
| O, cons a tl => Some a
| S p, cons a tl => nth_option A p tl
| n, nil => None
end.
Prove the following theorem:
Lemma nth_length :
forall (A:Set)(n:nat)(l:list A), nth_option _ n l = None <->
length l <= n.