congr 1
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))
case succ.e_a
S : Type
image_zero : S
image_succ : N → S → S
a b c n : N
hn : (a + b) * n = a * n + b * n
⊢ b * n + (a + b) = a + (b * n + b)