use 1
case zero

⊢ ∃ k, (Nat.digits 10 (2 ^ Nat.succ 0 * ↑k)).length = Nat.succ 0 ∧ all_one_or_two (Nat.digits 10 (2 ^ Nat.succ 0 * ↑k))
case h

⊢ (Nat.digits 10 (2 ^ Nat.succ 0 * ↑1)).length = Nat.succ 0 ∧ all_one_or_two (Nat.digits 10 (2 ^ Nat.succ 0 * ↑1))