English
Let α be a cancellative monoid with zero equipped with a partial order, and suppose left multiplication by a positive element reflects strict order. Then left multiplication by any positive element is monotone with respect to the non-strict order: if x ≤ y and 0 < a, then a·x ≤ a·y.
Русский
Пусть α — cancel-монад с нулём и частичным порядком; если умножение слева на положительный элемент отражает строгий порядок, то умножение слева на любой положительный элемент сохраняет нестрогое неравенство: если x ≤ y и 0 < a, то a·x ≤ a·y.
LaTeX
$$$\forall a\,x\,y\; (0 < a \land x \le y) \Rightarrow a \cdot x \le a \cdot y$$$
Lean4
theorem toMulPosReflectLE [MulPosReflectLT α] : MulPosReflectLE α where
elim := fun x _ _ h =>
h.eq_or_lt.elim (le_of_eq ∘ mul_right_cancel₀ x.2.ne.symm) fun h' => (lt_of_mul_lt_mul_right h' x.2.le).le
