lean_workbook_plus_21624

import Mathlib.Analysis.Complex.Basic

theorem lean_workbook_plus_21624 : ∀ a b c : ℝ, (b * c) / (b ^ 5 + c ^ 5 + b * c) + (c * a) / (c ^ 5 + a ^ 5 + c * a) + (a * b) / (a ^ 5 + b ^ 5 + a * b) ≤ 1   :=  by sorry