Definition 1.8.1.25.  Let n ∈ , m ∈ n. For x ∈ , we define:
n − m = x  :⇔  n = x + m
Well-definedness.  No proof.
References.