# The commutativity of addition.

There are two reasonably natural ways of proving this from
the Peano axioms. One is to prove associativity first (which
follows quickly from the definitions and induction), after
which the proof of commutativity is itself a straightforward
induction, and the other is the approach I take below. For html
reasons I use the letter s instead of sigma for the successor function.

### Lemma.

m+s(n)=s(m)+n for every m,n in N

### Proof.

As usual, we'll prove it first for n=1 and then for s(n)
assuming the result for n.

Step 1: m+s(1)=s(m+1)=s(s(m))=s(m)+1.

All these equalities follow from the definition of addition.

Step 2: Assume that m+s(n)=s(m)+n. Then

m+s(s(n))=s(m+s(n))=s(s(m)+n)=s(m)+s(n).

This time the first and third equalities were by the definition
of addition and the middle one was by the inductive hypothesis.

Now let's see how the lemma helps us out.

### Theorem.

m+n=n+m for every m,n in N.

### Proof

Again, this is by induction on n.

Step 1: m+1=1+m. This we prove by induction on m. True when
m=1. If true for m then

s(m)+1=m+s(1) by the lemma.

m+s(1)=s(m+1) by the definition of addition.

s(m+1)=s(1+m) by the induction hypothesis.

s(1+m)=1+s(m) by the definition of addition.

Step 2: Assume that m+n=n+m. We'd like to prove that
m+s(n)=s(n)+m. The proof is fairly similar to that of Step 1.

m+s(n)=s(m+n) by the definition of addition.

s(m+n)=s(n+m) by the inductive hypothesis.

s(n+m)=n+s(m) by the definition of addition.

n+s(m)=s(n)+m by the lemma.

Notice that no cleverness was needed to think of the
lemma - if you plunge straight in and try to prove commutativity
then you find you need the lemma, and if you plunge straight in
and try to prove the lemma then you succeed.