rw [mul_succ, mul_succ, hn, add_assoc, add_assoc, add_succ,
  add_succ, add_succ, add_succ, add_comm n a]
case succ
S : Type
image_zero : S
image_succ : N → S → S
a b c n : N
hn : succ a * n = a * n + n
⊢ succ a * succ n = a * succ n + succ n
no goals