The set of integers can be partitioned into the set of even numbers
and the set of odd numbers, see zeo4. Instead of defining new class
variables and to represent these sets, we use the idiom
to say that " is even" (which implies , see
evenelz) and to say that " is odd" (under the
assumption that ). The previously proven theorems about even and
odd numbers, like zneo, zeo, zeo2, etc. use different
representations, which are equivalent to the representations using the
divides relation, see evend2 and oddp1d2. The corresponding theorems
are zeneo, zeo3 and zeo4.