Cancellation of Addition, a forgotten property

I was working out a proof of a property of order among the integers in preparation for continuing this series when I realized that I had forgotten an important property of addition amongst the natural numbers: cancellation.

Cancellation says that if you have a+c = b+c, then a=b. It's wanted for both addition and multiplication of natural numbers (in the latter case, a*c = b*c implies a=b). It allows for the simplification of various expressions when you see the same thing on both sides of an equals sign.

I relied too much on my analysis book to list the properties of numbers. It gave additive inverses as a property of reals, which negates the need for additive cancellation.

It's easy to prove, given our definition of addition:

For the base case (c=1), you have: \[ a + 1 = b + 1 \Rightarrow S (a) = S (b) \Rightarrow a = b \] working basically with the definition of addition and with the injective property of the successor function.

For the inductive case, we get to assume a+c = b+c, and need to show this still holds for S(c). \[ \begin{eqnarray*} a + c & = & b + c\\ S (a + c) & = & S (b + c)\\ (a + c) + 1 & = & (b + c) + 1\\ a + (c + 1) & = & b + (c + 1)\\ a + S (c) & = & b + S (c) \end{eqnarray*} \]

Initially, I had done that backwards, starting with the last line and showing the first line. I think I have a tendency to do that, which is bad. In this case, and in many others, each step is an equivalence, not just an implication, which allows me to get away with it, but I need to keep an eye out for that mistake.