lean_workbook_plus_9622

import Mathlib.Analysis.Complex.Basic

theorem lean_workbook_plus_9622 {a b c : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hc : 0 ≤ c) : (a + b + c) * (a * b + b * c + c * a) ≥ 9 * a * b * c   :=  by sorry