proposition: Lemma nth_In : forall (n:nat) (l:list A) (d:A), n < length l -> In (nth n l d) l.
proof: Proof. unfold lt; intro n; induction n as [| n hn]; simpl; intro l. - destruct l; simpl; [ inversion 2 | auto ]. - destruct l; simpl. * inversion 2. * intros d ie; right; apply hn. now apply Nat.succ_le_mono. Qed.
imports: PeanoNat