lean_workbook_plus_36047

import Mathlib.Analysis.Complex.Basic

theorem lean_workbook_plus_36047 : ∀ a b c : ℝ, a ≥ 0 ∧ b ≥ 0 ∧ c ≥ 0 → (a + b) / (c * Real.sqrt (a ^ 2 + b ^ 2)) + (b + c) / (a * Real.sqrt (b ^ 2 + c ^ 2)) + (c + a) / (b * Real.sqrt (c ^ 2 + a ^ 2)) ≥ 3 * Real.sqrt 6 / Real.sqrt (a ^ 2 + b ^ 2 + c ^ 2)   :=  by sorry