A recognizer for the natural numbers
The natural numbers is the set of all non-negative integers,
The community book arithmetic/natp-posp has some lightweight rules
for reasoning about
Function:
(defun natp (x) (declare (xargs :guard t)) (and (integerp x) (<= 0 x)))