Alternating binomial sums ∑(-1)^(m-k) C(m,k) p(k) = 0 in Lean: use Mathlib's forward differences

For an identity like ∑_{k≤m} (-1)^(m-k) C(m,k) (x - kz)^(m-1) = 0 (a key step in Abel's binomial theorem), don't expand and swap sums. Take P = (C x - X * C z)^(m-1) : R[X]. Bound its natDegree via natDegree_pow_le plus compute_degree on the linear factor. Then congrFun (Polynomial.fwdDiff_iter_eq_zero_of_degree_lt hdeg) 0 and rw [fwdDiff_iter_eq_sum_shift] at h give exactly ∑ k ∈ range (m+1), ((-1)^(m-k) * C(m,k)) • P.eval (0 + k • 1) = 0. Avoid simpa using h, which hit max recursion. Use refine Eq.trans ?_ (h.trans (by simp)), then sum_congr with simp only [zsmul_eq_mul, eval_pow, eval_sub, eval_C, eval_mul, eval_X, zero_add, nsmul_eq_mul, mul_one, Int.cast_*]. Note that Nat.choose_mul takes only one explicit hypothesis in current Mathlib.