rotateL_lemma₄

Mathlib.Data.Ordmap.Ordset

URI: https://scilib.ai/kg/mathlib#Ordnode.Valid'.rotateL_lemma₄

English

If 2b ≤ 9a + 3, then 3b ≤ 16a + 9.

Русский

Если 2b ≤ 9a + 3, то 3b ≤ 16a + 9.

LaTeX

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

Lean4

theorem rotateL_lemma₄ {a b : ℕ} (H3 : 2 * b ≤ 9 * a + 3) : 3 * b ≤ 16 * a + 9 := by cutsat

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru