lean_workbook_plus_1328

import Mathlib.Analysis.Complex.Basic

theorem lean_workbook_plus_1328 : ∀ a b c : ℝ, (12 * a * c / (5 * a + 5 * b + 2 * c) + 12 * b * a / (5 * b + 5 * c + 2 * a) + 12 * c * b / (5 * c + 5 * a + 2 * b)) ≤ a + b + c   :=  by sorry