rw [pow_succ]
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
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 * 10))).sum = (Nat.digits 10 (x + 1)).sum