Bennett shifted half choose scaled eq int rat

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

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_shifted_half_choose_scaled_eq_int_rat (k h : ℕ) :
    (4 : ℚ) ^ h * Ring.choose ((k : ℚ) + 1 / 2) h =
      (bennettScaledHalfShiftInt k h : ℚ) := by sorry











end D1Bound5
end