cases' n' with n'
case h
n' : ℕ
ih : ∀ m < n', Nat.digits 10 (prepend_one m) = Nat.digits 10 m ++ [1]
⊢ Nat.digits 10 (prepend_one n') = Nat.digits 10 n' ++ [1]
case h.zero
ih : ∀ m < 0, Nat.digits 10 (prepend_one m) = Nat.digits 10 m ++ [1]
⊢ Nat.digits 10 (prepend_one 0) = Nat.digits 10 0 ++ [1]

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