English
If PosMulReflectLT holds and MulPosMono holds, then MulPosReflectLE holds: left multiplication by a positive element preserves LE when right-multiplication by a nonnegative factor is used.
Русский
Если выполняются PosMulReflectLT и MulPosMono, то выполняется MulPosReflectLE: умножение слева на положительный элемент сохраняет LE при правом умножении на неотрицательный множитель.
LaTeX
$$$[MulPosMono\ G_0] \Rightarrow MulPosReflectLE\ G_0$$$
Lean4
/-- For a group with zero, `PosMulReflectLT G₀`
allows us to upgrade `MulPosMono G₀` to `MulPosReflectLE G₀`.
The other implication holds without the `PosMulReflectLT G₀` assumption,
see `MulPosReflectLT.toMulPosStrictMono` for a stronger version below.
This theorem shows that in the presence of the assumption `PosMulReflectLT G₀`,
it makes no sense to optimize between assumptions `MulPosMono G₀`, `MulPosStrictMono G₀`,
`MulPosReflectLT G₀`, and `MulPosReflectLE G₀`. -/
theorem of_posMulReflectLT_of_mulPosMono [MulPosMono G₀] : MulPosReflectLE G₀ where
elim := by
rintro ⟨a, ha⟩ b c h
simpa [ha.ne'] using mul_le_mul_of_nonneg_right h (inv_nonneg.2 ha.le)
