Lean-Workbook Plus 4758: Exponential inequality

We have $\forall x\ge 1, e^{-x}\le 1\implies 1+e^{-x}\le 2\implies \frac{2}{x(1+e^{-x})}\ge \frac{1}{x}$

Source: Lean-Workbook row lean_workbook_plus_4758 (Apache-2.0). The unchanged proposition comes from the original record; its missing mathematical imports and namespaces are restored here.