lean_workbook_plus_77000

Proved

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

Prove that for positive reals, $\frac{x^3 + 1 +1 }{ 3} \ge x$ and $\frac{x^3 +x^3 +1}{3} \ge x^2$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_77000 (x : ℝ) (hx : 0 < x) : (x^3 + 1 + 1) / 3 ≥ x ∧ (x^3 + x^3 + 1) / 3 ≥ x^2   :=  by sorry

Source