lean_workbook_plus_77677

import Mathlib.Analysis.Complex.Basic

theorem lean_workbook_plus_77677 : ∀ a b c : ℝ, (a^2 * b * c ≠ 0 ∧ a * b * c ≠ 0) → b / c^2 + c / a^2 + a / b^2 ≥ 1 / a + 1 / b + 1 / c   :=  by sorry