Coerce an expected number to a number
Like fix, the-number logically returns its argument
unchanged if that argument is numeric and 0 otherwise. Unlike fix,
the guard for (the-number x) is (acl2-numberp x), and
(the-number x) evaluates to x in raw Lisp (see guards-and-evaluation for relevant discussion).
(defun the-number (x)
(declare (xargs :guard (acl2-numberp x)))
(mbe :logic (fix x) :exec x))