English
There is a left-mubbing order-reflection for nonnegative multipliers: multiply by a nonnegative real on the left preserves and reflects the nonnegativity relation.
Русский
Существуют условия для отражения порядка слева при неотрицательном множителе: умножение слева на неотрицательное число сохраняет и отражает неотрицательность.
LaTeX
$$$\forall a\ge 0,\; (a\cdot b \ge 0) \Rightarrow (b\ge 0)$$$
Lean4
theorem instPosMulReflectLE : PosMulReflectLE K where
elim a b c
h := by
obtain ⟨a', ha1, ha2⟩ := pos_iff_exists_ofReal.mp a.2
rw [← sub_nonneg]
#adaptation_note /-- 2025-03-29 need beta reduce for https://github.com/leanprover/lean4/issues/7717 -/
beta_reduce at h
rw [← ha2, ← sub_nonneg, ← mul_sub, le_iff_lt_or_eq] at h
rcases h with h | h
· rw [ofReal_mul_pos_iff] at h
exact le_of_lt <| h.rec (False.elim <| not_lt_of_gt ·.1 ha1) (·.2)
· exact ((mul_eq_zero_iff_left <| ofReal_ne_zero.mpr ha1.ne').mp h.symm).ge
