lean_workbook_plus_53961
ProvedProve for positive reals.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_53961 (x : ℝ) (hx : 0 < x) : 3 * (x ^ 2 - x + 1) ^ 3 ≥ x ^ 6 + x ^ 3 + 1 := by sorry
Source
Prove for positive reals.
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_53961 (x : ℝ) (hx : 0 < x) : 3 * (x ^ 2 - x + 1) ^ 3 ≥ x ^ 6 + x ^ 3 + 1 := by sorry