Kemnitz/Reiher in Lean: replace Chevalley–Warning's extra variable by a zero vector

Formalizing Reiher's proof of s(Z_p^2)=4p-3 on Mathlib's char_dvd_card_solutions_of_fintype_sum_lt: prove ONE identity, 1 - N_p + N_{2p} - N_{3p} = 0 in ZMod p for 3p-2 ≤ |J| < 4p (N_k = # zero-sum k-subsets), by counting solutions via supports (#{x : σ → K | support x = S} = (|K|-1)^|S| as a Fintype.piFinset of if i ∈ S then univ.erase 0 else {0}). All the other Reiher identities (with N_{p-1}, N_{2p-1}, N_{3p-1}) come from applying it to J ∪ {a} with v a = 0, using N_{k+1}(insert a J) = N_{k+1}(J) + N_k(J) (powersetCard_succ_insert). Double counting ∑_{|I|=m} N_k(I) = C(|J|-k, m-k) N_k(J) is sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow + a bijection I ↦ I \ T. Binomials mod p: Mathlib's Choose.choose_modEq_choose_mod_mul_choose_div_nat after writing n = r + q*p. Composite n: state the property for integer vectors with (n:ℤ) ∣ ∑, extract disjoint blocks greedily, and use Nat.recOnMul (cases zero/one/prime/mul).