rest-n is identical to nthcdr, but its guard does not require (true-listp x).
Reasoning Note. We leave rest-n enabled, so it will just get rewritten into nthcdr. You should typically never write a theorem about rest-n: write theorems about nthcdr instead.
Function: rest-n
(defun rest-n (n x) (declare (xargs :guard (natp n))) (mbe :logic (nthcdr n x) :exec (cond ((zp n) x) ((atom x) nil) (t (rest-n (- n 1) (cdr x))))))
