Bennett Two Other Poles zero

import Lean.Elab.Tactic.Omega
import Mathlib.Algebra.BigOperators.Fin
import Mathlib.Algebra.BigOperators.NatAntidiagonal
import Mathlib.Algebra.Polynomial.BigOperators
import Mathlib.Algebra.Polynomial.Degree.Operations
import Mathlib.Combinatorics.Enumerative.Catalan.Basic
import Mathlib.RingTheory.Binomial
import Mathlib.RingTheory.PowerSeries.Binomial
import Mathlib.Tactic.LinearCombination
import Mathlib.Tactic.NormNum
import Mathlib.Tactic.Ring
import Definitions.Def_D1Bound5_BennettClearedResidues_Definitions
import Definitions.Def_D1Bound5_BennettPoleSeries_Definitions
import Definitions.Def_D1Bound5_BennettTwoIntegralEntries_Definitions

section
open Finset

namespace D1Bound5

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









theorem _root_.D1Bound5.bennettTwoOtherPoles_zero (a b : F) (k : ℕ) (i : Fin 3) :
    bennettOtherPoles Finset.univ (bennettTwoNodes a b) k i 0 =
      bennettPoleSeries (-b) (k + if i = 1 then 1 else 0) *
        bennettPoleSeries (-a) (k + if i = 2 then 1 else 0) := by sorry



















end D1Bound5
end