Bennett catalan rat recurrence

import Mathlib.Algebra.BigOperators.NatAntidiagonal
import Mathlib.Combinatorics.Enumerative.Catalan.Basic
import Mathlib.RingTheory.Binomial
import Mathlib.Tactic.LinearCombination
import Mathlib.Tactic.NormNum

section
open Finset

namespace D1Bound5

/-!
The integer denominator bounds used in the Bennett residue construction.
The rational half-binomial identity is proved from the actual Catalan and
central-binomial identities in mathlib, then transported to every
characteristic-zero field. No coefficient-integrality premise is assumed.
-/


theorem _root_.D1Bound5.bennett_catalan_rat_recurrence (n : ℕ) :
    ((n : ℚ) + 2) * (catalan (n + 1) : ℚ) =
      2 * (2 * (n : ℚ) + 1) * (catalan n : ℚ) := by sorry























end D1Bound5
end