Lee-O'Sullivan Divisibility Helpers

Hasse-derivative and vanishing-polynomial divisibility bridges used in completeness.

theorem CompPoly.GuruswamiSudan.LeeOSullivan.coeffY_dvd_vanishingPolynomial_pow_of_multiplicity {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (V : CPolynomial.VanishingPolynomialContext F) {points : Array (F × F)} {P : CBivariate F} {m n : ℕ} (hdistinct : DistinctXCoordinates points) (hn : n < m) (hY : ∀ (j : ℕ), n < j → (↑P).coeff j = 0) (hmult : P.SatisfiesMultiplicityConstraints points m) : ∃ (W : CPolynomial F), (↑P).coeff n = W * V.vanishingPolynomial (Array.map (fun (point : F × F) => point.1) points) ^ (m - n)