lean_workbook_plus_61400

import Mathlib.Analysis.Complex.Basic

theorem lean_workbook_plus_61400 (a b c x y z : ℝ) (h1 : a ≥ b ∧ b ≥ c) (h2 : x ≥ y ∧ y ≥ z) (h3 : x + y + z = 0) : a * x + b * y + c * z ≥ 0   :=  by sorry