Not done with my proof.
So far I have proved "Add (0, x) = x" and "S(x) = Add (S(0), x)". I'm especially proud of that second one. No more hand wave.
I have also proved "Add (a, S(0)) = Add (S(0), a)".
So I have it proved for base cases b = 0 and b = S(0). I'm using induction, obvs, so I'm currently (so far unsuccessfully) working on how to prove "Add (a, b) = Add (b, a) implies Add (S(a), S(b)) = Add (S(b), S(a))"
Question: Once I get that done, am I done? What of "a"? I can write out the same proof using a instead of b, but how do I know that the proof works for both variables at the same time? If it does at all.