linarith
case inl
a b : ℤ
h : ∀ (x : ℤ), 2 * a ≤ x ∨ x ≤ 2 * b
h1 : 2 * a ≤ a + b
⊢ a ≤ b

case inr
a b : ℤ
h : ∀ (x : ℤ), 2 * a ≤ x ∨ x ≤ 2 * b
h2 : a + b ≤ 2 * b
⊢ a ≤ b
case inr
a b : ℤ
h : ∀ (x : ℤ), 2 * a ≤ x ∨ x ≤ 2 * b
h2 : a + b ≤ 2 * b
⊢ a ≤ b