lean_workbook_plus_64974
ProvedProve that given with .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_64974 (x y z : ℝ) (hx : x > 0) (hy : y > 0) (hz : z > 0) (habc : x * y * z = 1) : (x + 1) / (x ^ 2 + x + 1) + (y + 1) / (y ^ 2 + y + 1) + (z + 1) / (z ^ 2 + z + 1) ≤ 2 := by sorry
Source