node4L_lemma₄ — Mathlib

English

If a, b, c, d are natural numbers with three inequalities holding (lr1: 3a ≤ b + c + 1 + d, mr2: b + c + 1 ≤ 3d, mm1: b ≤ 3c), then a + b + 1 ≤ 3(c + d + 1).

Русский

Пусть a, b, c, d — натуральные числа и выполняются lr1: 3a ≤ b + c + 1 + d, mr2: b + c + 1 ≤ 3d, mm1: b ≤ 3c. Тогда a + b + 1 ≤ 3(c + d + 1).

LaTeX

$$$ \forall a,b,c,d \in \mathbb{N},\ (3a \le b+c+1+d) \land (b+c+1 \le 3d) \land (b \le 3c) \Rightarrow a+b+1 \le 3\,(c+d+1) $$$

Lean4

theorem node4L_lemma₄ {a b c d : ℕ} (lr₁ : 3 * a ≤ b + c + 1 + d) (mr₂ : b + c + 1 ≤ 3 * d) (mm₁ : b ≤ 3 * c) :
    a + b + 1 ≤ 3 * (c + d + 1) := by cutsat

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