lean_workbook_plus_71796

import Mathlib.Analysis.Complex.Basic

theorem lean_workbook_plus_71796 (a b c : ℝ) (ha : a > 0) (hb : b > 0) (hc : c > 0) : (1 / a + 1 / b + 1 / c ≥ 27 / 8) → (8 * a * b + 8 * b * c + 8 * c * a ≥ 27 * a * b * c)   :=  by sorry