A shifted cubic polynomial has a uniform lower difference bound

Proved

WorkbookSource.plus_38644

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

lean-workbooksource-checked

Prove that for real numbers $t, z$ with $t < z$ , $t^3 - 3t - 2 \leq (t + h)^3 - 3(t + h) + 2$ where $h > 0$

Source: InternLM Lean-Workbook, record lean_workbook_plus_38644 (Apache-2.0). Complete source proposition preserved; proof developed independently.

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.plus_38644 (t z h : ℝ) (hz : t < z) (hh : h > 0) : t^3 - 3 * t - 2 ≤ (t + h)^3 - 3 * (t + h) + 2   :=  by sorry

Source