rw [prepend_two_eq_append, all_one_or_two]
n : ℕ
hn : all_one_or_two (Nat.digits 10 n)
⊢ all_one_or_two (Nat.digits 10 (prepend_two n))
n : ℕ
hn : all_one_or_two (Nat.digits 10 n)
⊢ ∀ e ∈ Nat.digits 10 n ++ [2], e = 1 ∨ e = 2