Definition 1.8.1.36.  Let n ∈ . We define:
n is even  :⇔  {true if n = 0x is odd if n = x + 1 (x ∈ )  ⇔  2 ∣ n
n is odd  :⇔  n is not even
Equivalence.  No proof.
References.