Theorem: add'_comm (LAMR/Examples/using_lean_as_a_proof_assistant/induction.lean)

State before:
m n : ℕ
⊢ add' m n = add' n m
Tactic:
induction m with
| zero =>
  rw [zero_eq, zero_add', add']
| succ m ih =>
  rw [add', succ_add', ih]
State after:
no goals

State before:
case zero
n : ℕ
⊢ add' zero n = add' n zero
Tactic:
rw [zero_eq, zero_add', add']
State after:
no goals

State before:
case succ
n m : ℕ
ih : add' m n = add' n m
⊢ add' (succ m) n = add' n (succ m)
Tactic:
rw [add', succ_add', ih]
State after:
no goals