proposition: Lemma nth_error_past_end : forall (ls : list T) n, length ls <= n -> nth_error ls n = None.
proof: Proof. clear. induction ls; destruct n; simpl; intros; auto. + inversion H. + apply IHls. apply Nat.succ_le_mono; assumption. Qed.
imports: Coq.Lists.List Coq.Arith.PeanoNat