mul_ediv_le_mul_ediv_assoc — Mathlib

English

For integers a,b,c with a ≥ 0 and c ≥ 0, we have a·(b/c) ≤ (a·b)/c.

Русский

Для целых чисел a,b,c с a ≥ 0 и c ≥ 0 выполняется неравенство a·(b/c) ≤ (a·b)/c.

LaTeX

$$$0 \le a \land 0 \le c \Rightarrow a \cdot (b/c) \le (a \cdot b)/c$$$

Lean4

theorem mul_ediv_le_mul_ediv_assoc {a : Int} (ha : 0 ≤ a) (b : Int) {c : Int} (hc : 0 ≤ c) : a * (b / c) ≤ a * b / c :=
  by
  obtain rfl | hlt : c = 0 ∨ 0 < c := by cutsat
  · simp
  · rw [Int.le_ediv_iff_mul_le hlt, Int.mul_assoc]
    exact Int.mul_le_mul_of_nonneg_left (Int.ediv_mul_le b (Int.ne_of_gt hlt)) ha

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