Bennett Other Poles remove

import Lean.Elab.Tactic.Omega
import Mathlib.Algebra.Polynomial.BigOperators
import Mathlib.Algebra.Polynomial.Degree.Operations
import Mathlib.RingTheory.PowerSeries.Binomial
import Mathlib.Tactic.Ring
import Definitions.Def_D1Bound5_BennettClearedResidues_Definitions
import Definitions.Def_D1Bound5_BennettPoleSeries_Definitions

section
open Finset

namespace D1Bound5

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









section Nodes

variable {I : Type*} [DecidableEq I]








theorem _root_.D1Bound5.bennettOtherPoles_remove (s : Finset I) (a : I → F)
    (k : ℕ) (i j q : I) (hq : q ∈ s) (hiq : i ≠ q) (hjq : j ≠ q) :
    bennettOtherPoles s a k i j =
      bennettPoleSeries (a j - a q) k *
        bennettOtherPoles (s.erase q) a k i j := by sorry









end Nodes

end D1Bound5
end