add_le_mul_of_right_le_left — Mathlib

English

Let R be a semiring with 0 ≤ 1, NeZero 1, AddLeftMono, PosMulStrictMono. If 2 ≤ b and b ≤ a, then a + b ≤ a b.

Русский

Пусть R — полукольцо с 0 ≤ 1, NeZero 1, AddLeftMono и PosMulStrictMono. Если 2 ≤ b и b ≤ a, то a + b ≤ a b.

LaTeX

$$$(2 \le b) \land (b \le a) \Rightarrow a + b \le a b$$$

Lean4

theorem add_le_mul_of_right_le_left [ZeroLEOneClass R] [NeZero (1 : R)] [AddLeftMono R] [PosMulStrictMono R]
    (b2 : 2 ≤ b) (ba : b ≤ a) : a + b ≤ a * b :=
  have : 0 < a :=
    calc
      0
      _ < 2 := zero_lt_two
      _ ≤ b := b2
      _ ≤ a := ba
  calc
    a + b ≤ a + a := add_le_add_left ba a
    _ = a * 2 := (mul_two a).symm
    _ ≤ a * b := (mul_le_mul_iff_right₀ this).mpr b2

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