proposition: Theorem nth_error_length_ge : forall T (ls : list T) n, nth_error ls n = None -> length ls <= n.
proof: Proof. induction ls; destruct n; simpl in *; auto; simpl in *. + intro. apply Nat.le_0_l. + inversion 1. + intros. apply ->Nat.succ_le_mono. auto. Qed.
imports: Coq.Lists.List Coq.Arith.PeanoNat