A cubic inequality on the unit interval

Proved

WorkbookSource.problem_45148

by wamlart · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

lean-workbooksource-checked

Given the inequality $4(x^3 + 1) \geq (x + 1)^3 - (x - 1)^3$ for $x \in [0, 1)$ , prove that it is true.

Source: InternLM Lean-Workbook, record lean_workbook_45148; Apache-2.0. Complete source proposition preserved.

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.problem_45148 (x : ℝ) (hx : 0 ≤ x ∧ x < 1) :
  4 * (x^3 + 1) ≥ (x + 1)^3 - (x - 1)^3  :=  by sorry

Source