proposition: Theorem take_nth: forall i j r l, i < j \/ length l <= i -> nth i (take j l) r = nth i l r.
proof: Proof. intros i j r l; generalize i j r; elim l; simpl; auto with arith; clear i j r l. intros i j r; case i; auto; intros; rewrite take_nil; auto. intros a l Rec i j r; case i. case j; auto. intros [HH | HH]; contradict HH; auto with arith. intros n; case j; simpl; auto with arith. intros [HH | HH]. contradict HH; auto with arith. apply sym_equal; apply nth_default; auto with arith. intros n1 HH; apply Rec; case HH; auto with arith. Qed.
imports: List ListAux UList OrderedList