English
Let α be a type with a binary operation and a preorder, equipped with the properties that left multiplication by a positive element is strictly monotone and reflects strict order. Then for all b,c ∈ α, b · a < c · a if and only if b < c, whenever a > 0.
Русский
Пусть α — множество с бинарной операцией и предварительным порядком, где умножение слева на положительный элемент сохраняет строгую монотонность и отражает строгий порядок. Тогда для любых b, c ∈ α верно b · a < c · a тогда и только тогда, когда b < c, при условии a > 0.
LaTeX
$$$\\\\forall \\alpha\\,[Mul\\;\\alpha]\\,[Zero\\;\\alpha]\\,[Preorder\\;\\alpha]\\,[MulPosStrictMono\\;\\alpha]\\,[MulPosReflectLT\\;\\alpha],\\\\\\\\forall b,c\\in \\alpha, 0 < a \\rightarrow (b \\cdot a < c \\cdot a \\iff b < c).$$$
Lean4
@[simp]
theorem mul_lt_mul_iff_left₀ [MulPosStrictMono α] [MulPosReflectLT α] (a0 : 0 < a) : b * a < c * a ↔ b < c :=
@rel_iff_cov α>0 α (fun x y => y * x) (· < ·) _ _ ⟨a, a0⟩ _ _
