div_le_div'' — Mathlib

English

If a ≤ b and c ≤ d in an ordered commutative group with left-mono, then a/d ≤ b/c.

Русский

Если a ≤ b и c ≤ d в упорядоченной коммутативной группе с левой монотонностью, то a/d ≤ b/c.

LaTeX

$$$(a \le b) \land (c \le d) \implies \dfrac{a}{d} \le \dfrac{b}{c}$$$

Lean4

@[to_additive (attr := gcongr) sub_le_sub]
theorem div_le_div'' (hab : a ≤ b) (hcd : c ≤ d) : a / d ≤ b / c :=
  by
  rw [div_eq_mul_inv, div_eq_mul_inv, mul_comm b, mul_inv_le_inv_mul_iff, mul_comm]
  exact mul_le_mul' hab hcd

Похожие утверждения