Commutativity of addition says a + b = b + a. This is one of those facts that seems too obvious to need a proof — until you try to prove it from the definition of addition and realise it is genuinely harder than associativity.
The difficulty is that Nat.add recurses on its second argument. So a + succ b unfolds nicely (to succ (a + b)), but succ a + b does not. To handle the successor on the left, you need the lemma Nat.succ_add:
Nat.succ_add (n m : Nat) : succ n + m = succ (n + m)
Together with Nat.zero_add (which we proved in exercise 01) and Nat.add_succ, these lemmas let you shuffle successors between left and right until both sides match.
theorem my_add_comm (a b : Nat) : a + b = b + a := by sorry
Induct on b. In the base case you need a + 0 = 0 + a. The left side reduces by definition; the right side is Nat.zero_add.
In the successor case, you need to show a + succ b = succ b + a. Use Nat.add_succ to rewrite the left side and Nat.succ_add to rewrite the right side. Both become succ (something), and the induction hypothesis closes the gap.
theorem my_add_comm (a b : Nat) : a + b = b + a := by omega
theorem my_add_comm (a b : Nat) : a + b = b + a := by
induction b with
| zero => simp
| succ b ih =>
simp [Nat.add_succ, Nat.succ_add]
exact ih
In the base case, simp handles a + 0 = 0 + a using Nat.add_zero and Nat.zero_add. In the successor case, Nat.add_succ rewrites a + succ b to succ (a + b), and Nat.succ_add rewrites succ b + a to succ (b + a). Then ih : a + b = b + a finishes it.
Commutativity is harder than associativity. Associativity only needs induction on the recursion variable. Commutativity needs auxiliary lemmas (zero_add, succ_add) because you must move constructors across the operator.
Nat.succ_add and Nat.add_succ are the two workhorses for natural number proofs. Know them by name — you will use them constantly.
Building on earlier results. This proof depends on zero_add from exercise 01. Mathematics is cumulative: each theorem stands on the ones before it.