proposition: Theorem list_nth_in : ∀ A l n (d : A), (n < length l)%nat → List.nth n l d ∈ l.
proof: Proof. intros A l n d Hnl. revert n Hnl. induction l as [| x]; intros. exfalso; revert Hnl; apply Nat.nlt_0_r. simpl in Hnl. destruct n; [ left; reflexivity | simpl ]. apply Nat.succ_lt_mono in Hnl. right; apply IHl; assumption. Qed.
imports: Utf8 QArith NPeano Sorted Psatz