induction' n using Nat.strong_induction_on with n' ih
n : ℕ
⊢ Nat.digits 10 (prepend_two n) = Nat.digits 10 n ++ [2]
case h
n' : ℕ
ih : ∀ m < n', Nat.digits 10 (prepend_two m) = Nat.digits 10 m ++ [2]
⊢ Nat.digits 10 (prepend_two n') = Nat.digits 10 n' ++ [2]