lean_workbook_plus_78656
Proved,
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_78656 (x : ℝ) (h : x ≥ 1) : x^2 * (x - 1) ≥ x - 1 := by sorry
Source
,
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_78656 (x : ℝ) (h : x ≥ 1) : x^2 * (x - 1) ≥ x - 1 := by sorry