rw [prepend_one_div _ (Nat.succ_pos n')]
case h.succ
n' : ℕ
ih : ∀ m < n' + 1, Nat.digits 10 (prepend_one m) = Nat.digits 10 m ++ [1]
⊢ prepend_one (n' + 1) % 10 :: Nat.digits 10 (prepend_one (n' + 1) / 10) = Nat.digits 10 (n' + 1) ++ [1]
case h.succ
n' : ℕ
ih : ∀ m < n' + 1, Nat.digits 10 (prepend_one m) = Nat.digits 10 m ++ [1]
⊢ prepend_one (n' + 1) % 10 :: Nat.digits 10 (prepend_one (n'.succ / 10)) = Nat.digits 10 (n' + 1) ++ [1]