lean_workbook_plus_70024

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

If a,b are natural numbers with $a\\ge b$ , then show that: \n $(b+1)(b+2)(a-b+1)(a-b+2)\\ge2(a+1)(a+2).$ \nIt holds for all $a \\ge b \\ge 1$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_70024 (a b : ℕ) (h₁ : 1 ≤ b) (h₂ : b ≤ a) :  (b + 1) * (b + 2) * (a - b + 1) * (a - b + 2) ≥ 2 * (a + 1) * (a + 2)   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph