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

State before:
a b : ℤ
h : ∀ (x : ℤ), 2 * a ≤ x ∨ x ≤ 2 * b
⊢ a ≤ b
Tactic:
sorry
State after:
no goals