lean_workbook_plus_7923
ProvedProve $\frac{1}{\frac{1}{1+a}+\frac{1}{1+b}+\frac{1}{1+c}}-\frac{1}{\frac{1}{a}+\frac{1}{b}+\frac{1}{c}}\geq \frac{1}{3}$ for arbitrary positive reals $a, b, c.$ Is there a clean way to solve this problem without expanding?
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_7923 (a b c : ℝ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : (1 / (1 / (1 + a) + 1 / (1 + b) + 1 / (1 + c)) - 1 / (1 / a + 1 / b + 1 / c)) ≥ 1 / 3 := by sorry
Source