intro h
α : Type
inst✝ : LinearOrderedField α
x y a b : α
⊢ x * y ≥ b * x + a * y - a * b → x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b
α : Type
inst✝ : LinearOrderedField α
x y a b : α
h : x * y ≥ b * x + a * y - a * b
⊢ x ≤ a ∧ y ≤ b ∨ x ≥ a ∧ y ≥ b