(rw [mul_succ])
case succ
a b c' : Nat
ih : a * b * c' = a * (b * c')
⊢ a * b * c' + a * b = a * (b * succ c')
case succ
a b c' : Nat
ih : a * b * c' = a * (b * c')
⊢ a * b * c' + a * b = a * (b * c' + b)