lean_workbook_plus_60849
ProvedProve for all .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_60849 (y : ℝ) (hy : y > 0) : y ^ 3 + 4 * y + 2 / y - 2 * y ^ 2 ≥ 4 := by sorry
Source
Prove for all .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_60849 (y : ℝ) (hy : y > 0) : y ^ 3 + 4 * y + 2 / y - 2 * y ^ 2 ≥ 4 := by sorry