induction' n using Nat.strong_induction_on with n' ih
n : ℕ
⊢ Nat.digits 10 (prepend_one n) = Nat.digits 10 n ++ [1]
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]