lean_workbook_plus_37958

import Mathlib.Analysis.Complex.Basic

theorem lean_workbook_plus_37958 : ∀ a b c : ℝ, 2 * (a ^ 5 + b ^ 5 + c ^ 5) ≥ a * b ^ 4 + b * c ^ 4 + c * a ^ 4 + a ^ 4 * b + b ^ 4 * c + c ^ 4 * a   :=  by sorry