lean_workbook_plus_31978

import Mathlib.Analysis.Complex.Basic

theorem lean_workbook_plus_31978 {a b c : ℝ} (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : (1 / (a * b) + 1 / (b * c) + 1 / (c * a)) ≥ 9 / (a * b + b * c + c * a)   :=  by sorry