lean_workbook_plus_76620

import Mathlib.Analysis.Complex.Basic

theorem lean_workbook_plus_76620 (a b c x y z : ℝ) (h₁ : a ≥ b ∧ b ≥ c) (h₂ : x ≥ y ∧ y ≥ z) (h₃ : x + y + z = 0) : a * x + b * y + c * z ≥ 0   :=  by sorry