lean_workbook_plus_57471

import Mathlib.Analysis.Complex.Basic

theorem lean_workbook_plus_57471 (a b c d : ℝ) (ha : a ≥ 0) (hb : b ≥ 0) (hc : c ≥ 0) (hd : d ≥ 0) : a ^ 3 + b ^ 3 + c ^ 3 + d ^ 3 ≥ a * b * c + b * c * d + c * d * a + d * a * b   :=  by sorry