change a * (0 + c) = a * 0 + a * c
case zero
S : Type
image_zero : S
image_succ : N → S → S
a b c : N
⊢ a * (zero + c) = a * zero + a * c
case zero
S : Type
image_zero : S
image_succ : N → S → S
a b c : N
⊢ a * (0 + c) = a * 0 + a * c