rw [Nat.digits_def' two_le_ten (prepend_two_pos _)]
case h.succ
n' : ℕ
ih : ∀ m < n' + 1, Nat.digits 10 (prepend_two m) = Nat.digits 10 m ++ [2]
⊢ Nat.digits 10 (prepend_two (n' + 1)) = 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]
⊢ prepend_two (n' + 1) % 10 :: Nat.digits 10 (prepend_two (n' + 1) / 10) = Nat.digits 10 (n' + 1) ++ [2]