simp at xaNeg'
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaNeg : x - a < 0
ybPos : 0 < y - b
xaNeg' : x - a ≤ 0
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaNeg : x - a < 0
ybPos : 0 < y - b
xaNeg' : x ≤ a
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b