lean_workbook_plus_64526

Proved

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

Prove that $f(k)=k^{3}-2k^{2}+k+1>0$ when $k \geq \frac{1}{2}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_64526 (k : ℝ) (h : k >= 1/2) : k^3 - 2 * k^2 + k + 1 > 0   :=  by sorry

Source