lean_workbook_plus_16357
ProvedIf positive reals, then .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_16357 (x y : ℝ) (hx : 0 < x) (hy : 0 < y) : x^3 + y^3 + 2 ≥ 2 * x * y + x + y := by sorry
Source
If positive reals, then .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_16357 (x y : ℝ) (hx : 0 < x) (hy : 0 < y) : x^3 + y^3 + 2 ≥ 2 * x * y + x + y := by sorry