lean_workbook_plus_21717

import Mathlib.Analysis.Complex.Basic

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