lean_workbook_plus_30565

import Mathlib.Analysis.Complex.Basic

theorem lean_workbook_plus_30565 : ∀ a b c : ℝ, a > 0 ∧ b > 0 ∧ c > 0 → a * b / (2 * c + a + b) ≤ a * b / 4 * (1 / (c + a) + 1 / (c + b))   :=  by sorry