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