rw [←List.cons_append]
case h.succ
n' : ℕ
ih : ∀ m < n' + 1, Nat.digits 10 (prepend_two m) = Nat.digits 10 m ++ [2]
hns : n'.succ / 10 < n'.succ
⊢ prepend_two (n' + 1) % 10 :: (Nat.digits 10 (n'.succ / 10) ++ [2]) = Nat.digits 10 (n' + 1) ++ [2]
case h.succ
n' : ℕ
ih : ∀ m < n' + 1, Nat.digits 10 (prepend_two m) = Nat.digits 10 m ++ [2]
hns : n'.succ / 10 < n'.succ
⊢ prepend_two (n' + 1) % 10 :: Nat.digits 10 (n'.succ / 10) ++ [2] = Nat.digits 10 (n' + 1) ++ [2]