Definition 1.8.1.14.  Let m, n ∈ . We define:
m ≤ n  :⇔  ∃ x ∈  : m + x = n  ⇔  {true if m = 0y ≤ n and y ≠ n if m = y + 1 (y ∈ )  ⇔  m = n or {false if n = 0m ≤ z if n = z + 1 (z ∈ )
Equivalence.  No proof.
References.