rw [mul_div_cancel_right₀ _ (by norm_num), List.length_cons]
case succ
m : ℕ
ih : (Nat.digits 10 (10 ^ m)).length = m + 1
⊢ (10 ^ m * 10 % 10 :: Nat.digits 10 (10 ^ m * 10 / 10)).length = m + 1 + 1
case succ
m : ℕ
ih : (Nat.digits 10 (10 ^ m)).length = m + 1
⊢ (Nat.digits 10 (10 ^ m)).length.succ = m + 1 + 1