exact Or.inr (And.intro xaPos' ybNeg')
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≤ b * x + a * y - a * b
h₁ : (x - a) * (y - b) ≤ 0
xaPos : 0 < x - a
ybNeg : y - b < 0
xaPos' : a ≤ x
ybNeg' : y ≤ b
⊢ x ≤ a ∧ y ≥ b ∨ x ≥ a ∧ y ≤ b
no goals