lean_workbook_plus_28241
ProvedLet . Prove that
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_28241 (x y z : ℝ) (h : x ≥ y ∧ y ≥ z ∧ z > 0) : x / (x + y) + y / (y + z) + z / (z + x) ≥ 3 / 2 := by sorry
Source