lean_workbook_plus_64530

Proved

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

${a_{n+2}\over 3}={(n+3)a_{n+1}\over 3(n+1)}\iff {a_{n+2}\over(n+2)(n+3)}={a_{n+1}\over(n+1)(n+2)}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_64530 (a : ℕ → ℝ) (n : ℕ) :
  a (n + 2) / 3 = ((n + 3) * a (n + 1)) / (3 * (n + 1)) ↔
  a (n + 2) / ((n + 2) * (n + 3)) = a (n + 1) / ((n + 1) * (n + 2))   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph