Definition 1.8.4.8.  Let a, b ∈ . We define
a ≤ b
by:
(na-ma) ≤ (nb-mb)  :⇔  na + mb ≤ nb + ma  (na, ma ∈ , nb, mb ∈ )  ⇔  ∃ x ∈  : a + x = b
Equivalence.  No proof.
Well-definedness.  No proof.
Remarks.

Note that the comparison on the right is comparison on natural numbers.

References.