lean_workbook_plus_73836
ProvedProve that .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_73836 {a c : ℝ} (ha : 0 < a) (hc : 0 < c) : (1 / c + 1 / a) / 2 ≥ 2 / (c + a) := by sorrySource
Prove that .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_73836 {a c : ℝ} (ha : 0 < a) (hc : 0 < c) : (1 / c + 1 / a) / 2 ≥ 2 / (c + a) := by sorry