A reciprocal sum with a nested reciprocal is at least five halves

Proved

WorkbookSource.base_20041

by wamlart · Sep 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

lean-workbooksource-checked

For positive real $a$ , prove that $a + \frac{1}{a} + \frac{1}{a + \frac{1}{a}} \geq \frac{5}{2}$ .

Source: InternLM Lean-Workbook, record lean_workbook_20041 (Apache-2.0). Complete source proposition preserved; proof developed independently.

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.base_20041 (a : ℝ) (ha : 0 < a) : a + (1/a) + (1/(a + (1/a))) ≥ 5/2  :=  by sorry

Source