Bennett shifted half choose uniform is integer

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_shifted_half_choose_uniform_is_integer
    {F : Type*} [Field F] [CharZero F] (k h K : ℕ) (hh : h ≤ K) :
    ∃ z : ℤ, (4 : F) ^ K * Ring.choose ((k : F) + 1 / 2) h = (z : F) := by sorry





end D1Bound5
end