proposition: Lemma nth_length {A : Type} : forall (n:nat)(l:list A), nth_option n l = None <-> length l <= n.
proof: Proof. induction n as [| p IHp]. - destruct l; simpl; split; auto. + discriminate 1. + inversion 1. - intro l; destruct l as [ | a l']. + split;simpl; auto with arith. + simpl; rewrite (IHp l'); split; auto with arith. Qed.
imports: List Arith