English
Let α be a type with multiplication, zero, and a preorder. If a > 0 and left multiplication by a is order-preserving and reflects ≤, then b · a ≤ c · a iff b ≤ c for all b,c ∈ α.
Русский
Пусть α — множество с умножением, нулем и предварительным порядком. Если a > 0 и умножение слева на a сохраняет порядок по отношению к ≤ и отражает ≤, то для любых b, c ∈ α выполняется b · a ≤ c · a тогда и только тогда, когда b ≤ c.
LaTeX
$$$\\\\forall \\alpha\\,[Mul\\;\\alpha]\\,[Zero\\;\\alpha]\\,[Preorder\\;\\alpha]\\,[PosMulMono\\;\\alpha]\\,[PosMulReflectLE\\;\\alpha],\\\\\\\\forall a,b,c\\in \\alpha, 0 < a \\rightarrow (a \\cdot b \\le a \\cdot c \\iff b \\le c).$$$
Lean4
@[simp]
theorem mul_le_mul_iff_right₀ [PosMulMono α] [PosMulReflectLE α] (a0 : 0 < a) : a * b ≤ a * c ↔ b ≤ c :=
@rel_iff_cov α>0 α (fun x y => x * y) (· ≤ ·) _ _ ⟨a, a0⟩ _ _
