lean_workbook_plus_72246

Proved

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

Let $a,b\geq 0$ and $(a+1)(ab^2+1) \geq 4.$ Prove that \n

a+b\geq 2

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_72246 (a b : ℝ) (ha : a ≥ 0) (hb : b ≥ 0) (hab : (a + 1) * (a * b ^ 2 + 1) ≥ 4) : a + b ≥ 2   :=  by sorry

Source