Theorem 7.3: Let a, b, and c be natural numbers with b < a. Then

if and only if

Proof: By Theorem 6.1, it suffices to show that

and

Since

by Definition 4.6 and therefore

by Theorem 2.11, and the result follows from Theorem 7.2.

For the converse, assume that c + b = a. By Theorem 6.3, the commutativity of addition,

so by Definition 6.1, a is obtained by taking successive successors of b. Since by Definition 4.3,, and Theorem 1.2, it follows that any number is contained in its successor, and, hence by Definition 4.6, any number is less than it successor. Therefore, by Theorem 4.5c, the transitivity of less than,

Thus, as we have just seen,

and

so by Theorem 6.1,

But we are assuming that

so

by Theorem 7.1, the cancellation property of addition.