lean_workbook_plus_55989

import Mathlib.Analysis.Complex.Basic

theorem lean_workbook_plus_55989 (a b c : ℝ) : a ^ 4 * b ^ 2 + b ^ 4 * c ^ 2 + c ^ 4 * a ^ 2 ≥ a * b ^ 2 * c ^ 3 + b * c ^ 2 * a ^ 3 + c * a ^ 2 * b ^ 3   :=  by sorry