Bennett Choose ne zero of avoids naturals

import Lean.Elab.Tactic.Omega
import Mathlib.RingTheory.Binomial
import Mathlib.Tactic.LinearCombination

section
open Polynomial

namespace D1Bound5

variable {F : Type*} [Field F] [CharZero F]


theorem _root_.D1Bound5.bennettChoose_ne_zero_of_avoids_naturals (r : F) (k : ℕ)
    (h : ∀ j : ℕ, j < k → r ≠ (j : F)) : Ring.choose r k ≠ 0 := by sorry





end D1Bound5
end