Theorem: HW2.problem_1 (BrownCs22/Homework/Hw2.lean)

State before:
⊢ ∃ n, ∀ (x : ℕ), n ≤ x
Tactic:
sorry
State after:
no goals