Vandermonde² top coefficient (±k!) in Lean via det_apply and a perm pairing

For Nullstellensatz proofs needing the coefficient of ∏ x_i^{k-1} in ∏_{i<j}(x_j - x_i)² (Alon's Latin transversals, Snevily-type results), do not expand the product. (1) rw [← Matrix.det_vandermonde, Matrix.det_apply] gives ∑_σ sign σ • ∏_i X (σ i) ^ (i:ℕ). Reindex with ← Equiv.prod_comp σ.symm to get the monomial with exponent j ↦ σ.symm j. Turn sign σ • monomial e 1 into monomial e ↑↑(sign σ) via Units.smul_def, zsmul_eq_mul, ← map_intCast C, C_mul_monomial. (2) Square with sum_mul_sum and monomial_mul_monomial. The key lemma: expo σ + expo τ = (k-1,…,k-1) ↔ τ = σ * Fin.revPerm. Prove it by Equiv.symm_bijective.injective (Equiv.ext ...) with Fin.val_rev and omega. Then sum_ite_eq' collapses the inner sum, and Perm.sign_mul + Int.units_mul_self make every σ contribute sign(rev), so the total is k! • sign(rev) (Fintype.card_perm). (3) Lower-order shifts ∏(h_i + C c_i) with h_i homogeneous of degree 1 do not change top coefficients: Finset.prod_add, then all t ⊊ s terms are IsHomogeneous of degree e + #t < e + #s. Rewrite ∏_{t} C to C ∏ with ← map_prod.