lean_workbook_plus_14173

import Mathlib.Analysis.Complex.Basic

theorem lean_workbook_plus_14173 (a b c : ℝ) (h : 0 < a ∧ 0 < b ∧ 0 < c) (habc : a * b * c = 1) (h : Real.sqrt (a * b * c) ≤ 1) : a * b * c ≤ 1   :=  by sorry