induction' m with m ih
case succ
m x : ℕ
⊢ (Nat.digits 10 ((x + 1) * 10 ^ m)).sum = (Nat.digits 10 (x + 1)).sum
case succ.zero
x : ℕ
⊢ (Nat.digits 10 ((x + 1) * 10 ^ 0)).sum = (Nat.digits 10 (x + 1)).sum

case succ.succ
x m : ℕ
ih : (Nat.digits 10 ((x + 1) * 10 ^ m)).sum = (Nat.digits 10 (x + 1)).sum
⊢ (Nat.digits 10 ((x + 1) * 10 ^ (m + 1))).sum = (Nat.digits 10 (x + 1)).sum