Some theorems about the built-in function last.
Theorem: last-of-cdr
(defthm last-of-cdr (equal (last (cdr x)) (if (consp (cdr x)) (last x) (cdr x))))
