Kummer's digit formula for central binomial coefficients

This module specializes Kummer's theorem to Nat.centralBinom, providing the arithmetic bridge used by the odd-prime carry enumerator.

theorem OddPrimeValuationDistribution.sub_one_mul_padicValNat_centralBinom (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) : (p - 1) * padicValNat p n.centralBinom = 2 * (p.digits n).sum - (p.digits (2 * n)).sum

Kummer's digit-sum formula specialized to central binomial coefficients.