Recognizer for naturals and nil.
This is like an option type; when x
satisfies maybe-natp, then either it is a natural number or nothing.
(defun maybe-natp$inline (x)
(declare (xargs :guard t))
(or (not x) (natp x)))
(equal (maybe-natp x)
(or (not x)
(and (integerp x) (<= 0 x))))