Major Section: ACL2-BUILT-INS
(posp x) is logically equivalent to
(not (zp x)) (see zp) and also
(and (natp x) (not (equal x 0))). We recommend the file
books/ordinals/natp-posp as a book for reasoning about
natp. This book is included in
To see the ACL2 definition of this function, see pf.