lean_workbook_plus_56424

import Mathlib.Analysis.Complex.Basic

theorem lean_workbook_plus_56424 (a b c : ℝ) (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0) : 1 / a ^ 2 + 1 / b ^ 2 + 1 / c ^ 2 ≥ (a + b + c) / (a * b * c)   :=  by sorry