node4L_lemma₅ — Mathlib

English

Let a, b, c, d be natural numbers with lr2: 3(b+c+1+d) ≤ 16a + 9, mr1: 2d ≤ b+c+1, mm2: c ≤ 3b. Then c + d + 1 ≤ 3(a + b + 1).

Русский

Пусть a, b, c, d — натуральные числа и выполняются lr2: 3(b+c+1+d) ≤ 16a + 9, mr1: 2d ≤ b+c+1, mm2: c ≤ 3b. Тогда c + d + 1 ≤ 3(a + b + 1).

LaTeX

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

Lean4

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

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