rw [ih _ hns]
case h.succ
n' : ℕ
ih : ∀ m < n' + 1, Nat.digits 10 (prepend_one m) = Nat.digits 10 m ++ [1]
hns : n'.succ / 10 < n'.succ
⊢ prepend_one (n' + 1) % 10 :: Nat.digits 10 (prepend_one (n'.succ / 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]
hns : n'.succ / 10 < n'.succ
⊢ prepend_one (n' + 1) % 10 :: (Nat.digits 10 (n'.succ / 10) ++ [1]) = Nat.digits 10 (n' + 1) ++ [1]