lean_workbook_plus_31271

Proved

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

Prove that for all positive real $x$ , the following inequality holds: \n\n

(x + 1)(x + 2)(x + 5) \geq 36x.

\n\n Okay this is Another solution

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_31271 (x : ℝ) (hx : 0 < x) : (x + 1) * (x + 2) * (x + 5) ≥ 36 * x   :=  by sorry

Source