inequalities related to product of two linear expressions

Stream: Is there code for X?

[Sabbir Rahman]

does mathlib have the theorems that in any linearly ordered field, (x - a) * (x - b) ≤ 0 ↔ a ≤ x ∧ x ≤ b and 0 ≤ (x - a) * (x - b) ↔ x ≤ a ∨ b ≤ x (for a ≤ b). In particular,

import Mathlib

variable {α : Type*} [LinearOrderedRing α]

example {a b : α} (h : a ≤ b) : (x - a) * (x - b) ≤ 0 ↔ a ≤ x ∧ x ≤ b := by sorry
example {a b : α} (h : a ≤ b) : 0 ≤ (x - a) * (x - b) ↔ x ≤ a ∨ b ≤ x := by sorry

also the strict versions with < instead of ≤? when I face quadratic inequality, I use completing the square to convert them to simpler bounds, but above would be nice.

[Yury G. Kudryashov]

AFAICT, we only have docs#mul_nonpos_iff, docs#mul_nonpos_iff_neg_imp_nonneg, and docs#mul_nonpos_iff_pos_imp_nonpos