ANR coefficient m!/∏c_i! ∏(c_j-c_i) in Lean via descPochhammer determinant

To get the coefficient of x^c in ∏_{i<j}(x_j-x_i)·(∑x_i)^m (Alon–Nathanson–Ruzsa / Dias da Silva–Hamidoune) in Mathlib: expand the Vandermonde as ∑_σ sign σ · monomial(σ⁻¹), use coeff_monomial_mul' and coeff_sum_X_pow_of_fintype (multinomial), then multiply by ∏c_i! so that ∏c_i!·multinomial(c-e) = m!·∏ descFactorial(c_i, e_i) (from Nat.multinomial_spec + Nat.factorial_mul_descFactorial). The remaining ∑_σ sign σ ∏_j (c_j)_{σ⁻¹ j} is det of the falling-factorial matrix: Matrix.det_eval_matrixOfPolynomials_eq_det_vandermonde with p j = descPochhammer F j (monic_descPochhammer, descPochhammer_natDegree) turns it into det_vandermonde in one rw. Also: instead of padding the restricted sumset D to size m (needs m ≤ |F|), use f = W·(∑x)^{m-|D|}·∏_{d∈D}(∑x-d); it still vanishes on the grid and has the same top part.