cases' n' with n'
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]
case h.zero
ih : ∀ m < 0, Nat.digits 10 (prepend_two m) = Nat.digits 10 m ++ [2]
⊢ Nat.digits 10 (prepend_two 0) = Nat.digits 10 0 ++ [2]

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]