proposition: Lemma nth_error_length_lt : forall {T} (ls : list T) n val, nth_error ls n = Some val -> n < length ls.
proof: Proof. induction ls; destruct n; simpl; intros; auto. + inversion H. + inversion H. + apply Nat.lt_0_succ. + apply ->Nat.succ_lt_mono. apply IHls with (1 := H). Qed.
imports: Coq.Lists.List Coq.Arith.PeanoNat