lean_workbook_plus_26296

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Given the sequence $x_{n+1} = 2 - \frac{1}{x_n}$ with $x_1 > 1$ , prove that $x_1 > x_2$ and that the sequence converges to 1.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_26296 (x : ℕ → ℝ) (hx : ∀ n, x (n + 1) = 2 - 1 / x n) (h : x 1 > 1) : x 1 > x 2   :=  by sorry

Source