add_le_mul_two_add — Mathlib

English

If a2 ≥ 2 and b0 ≥ 0 in a suitable ordered semiring, then a + (2 + b) ≤ a*(2 + b).

Русский

Если a ≥ 2 и b ≥ 0 в упорядоченном полукольце, то a + (2 + b) ≤ a(2 + b).

LaTeX

$$$2 \le a \Rightarrow 0 \le b \Rightarrow a + (2 + b) \le a \cdot (2 + b)$$$

Lean4

theorem add_le_mul_two_add [ZeroLEOneClass R] [MulPosMono R] [AddLeftMono R] (a2 : 2 ≤ a) (b0 : 0 ≤ b) :
    a + (2 + b) ≤ a * (2 + b) :=
  calc
    a + (2 + b) ≤ a + (a + a * b) :=
      add_le_add_left (add_le_add a2 <| le_mul_of_one_le_left b0 <| one_le_two.trans a2) a
    _ ≤ a * (2 + b) := by rw [mul_add, mul_two, add_assoc]

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