ACL2(r) recognizer for infinitesimal numbers
(I-small x) is true if and only if x is an infinitesimal number (possibly 0). This predicate is only defined in ACL2(r) (see real).
