lean_workbook_plus_37288
ProvedShow that the expression is nonegative, for every
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_37288 (x : ℝ) (hx: 1 ≤ x) : x^3 - 5 * x^2 + 8 * x - 4 ≥ 0 := by sorry
Source
Show that the expression is nonegative, for every
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_37288 (x : ℝ) (hx: 1 ≤ x) : x^3 - 5 * x^2 + 8 * x - 4 ≥ 0 := by sorry