(posp x) is logically equivalent to (not (zp x)) (see zp) and also
to (and (natp x) (not (equal x 0))). We recommend the file
books/ordinals/natp-posp as a book for reasoning about posp and
natp. This book is included in books/arithmetic/top and
books/arithmetic/top-with-meta.
