lean_workbook_plus_5725
ProvedPreamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_5725 (y z : ℝ) (hy : y > 0) (hz : z > 0) : (y + z) / (4 * y * z) ≥ 1 / (y + z) := by sorry
Source
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_5725 (y z : ℝ) (hy : y > 0) (hz : z > 0) : (y + z) / (4 * y * z) ≥ 1 / (y + z) := by sorry