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