Prove2Me

lean_workbook_plus_37054

Proved

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

Now let xn=an+1x_n = a_n + 1 . We have

xn+2=xnxn+12xn+1+xn(xn−1)  ⟹  xn+1xn+2=1xn+xnxn+1−1xn+1  ⟹  xn+1xn+2+1xn+1=xnxn+1+1xnx_{n+2} = \frac{x_nx_{n+1}^2}{x_{n+1} + x_n(x_n - 1)} \implies \frac{x_{n+1}}{x_{n+2}} = \frac{1}{x_n} + \frac{x_n}{x_{n+1}} - \frac{1}{x_{n+1}} \implies \frac{x_{n+1}}{x_{n+2}} + \frac{1}{x_{n+1}} = \frac{x_n}{x_{n+1}} + \frac{1}{x_n}
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_37054  (x : ℕ → ℝ)
  (n : ℕ)
  (h₀ : 0 < x (n + 1))
  (h₁ : 0 < x (n + 2))
  (h₂ : 0 < x n)
  (h₃ : x (n + 2) = (x n * (x (n + 1))^2) / (x (n + 1) + x n * (x n - 1))) :
  x (n + 1) / x (n + 2) + 1 / x (n + 1) = x n / x (n + 1) + 1 / x n   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph