(dec-induct n) is classic natural-number induction on n; we just subtract 1 until reaching 0.
Function: dec-induct
(defun dec-induct (n) (if (zp n) nil (dec-induct (- n 1))))
