lean_workbook_plus_27878

import Mathlib.Analysis.Complex.Basic

theorem lean_workbook_plus_27878 :  ∀ a b c : ℝ, a ≥ b ∧ b ≥ c ∧ c ≥ 0 → (b + c) / (a ^ 2 + b * c) + (c + a) / (b ^ 2 + c * a) + (a + b) / (c ^ 2 + a * b) ≥ 9 / (a + b + c)   :=  by sorry