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.
Definitions and Theorems
(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))))))