Bennett half choose scaled catalan

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_half_choose_scaled_catalan (n : ℕ) :
    (4 : ℚ) ^ (n + 1) * Ring.choose (1 / 2 : ℚ) (n + 1) =
      (-1 : ℚ) ^ n * 2 * (catalan n : ℚ) := by sorry



















end D1Bound5
end