proposition: Theorem jump_nth: forall l k r, nth k l r = nth 0 (jump k l) r.
proof: Proof. intros l; elim l; simpl; auto. intros k r; rewrite jump_nil; simpl; case k; auto. intros a l1 Rec k r; case k; simpl; auto. Qed.
imports: List ListAux UList OrderedList