rw [pow_succ]
case succ
m : ℕ
ih : (Nat.digits 10 (10 ^ m)).length = m + 1
⊢ (Nat.digits 10 (10 ^ (m + 1))).length = m + 1 + 1
case succ
m : ℕ
ih : (Nat.digits 10 (10 ^ m)).length = m + 1
⊢ (Nat.digits 10 (10 ^ m * 10)).length = m + 1 + 1