rw [prepend_one_mod _ (Nat.succ_pos _), Nat.digits_def' two_le_ten (Nat.succ_pos n')]
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]
no goals