lean_workbook_plus_42875

import Mathlib.Analysis.Complex.Basic

theorem lean_workbook_plus_42875 (a b c : ℝ) : (a / (b + c) + b / (c + a) + c / (a + b) ≥ 3 / 2 ∧ (a = b ∧ b = c ∧ c = 3 / 2)) ↔ a = b ∧ b = c ∧ c = 3 / 2   :=  by sorry