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