> We develop the theory of the Peano numbers, define addition, and prove that addition is commutative, Was that because we didn't know how to do addition? No. We already knew that addition was commutative. The point of the theorem is to show that Peano arithmetic knows that addition is commutative.

Gotta remember this when the kiddo starts doing proofs.