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