Prime-row binomial coefficient divisibility ($p\mid \left(\genfrac{}{}{0ex}{}{p}{r}\right)(0<r<p)$)

For a prime number $p$, the identity $r!\left(\genfrac{}{}{0ex}{}{p}{r}\right)=p(p-1)\cdots (p-r+1)$ has right side divisible by $p$, while $r!$ is coprime to $p$. Cancellation in modular arithmetic proves the divisibility.

// Target: combinatorics.bigb

In polynomial modular arithmetic, prime-row binomial coefficient divisibility gives $(1+X{)}^p\equiv 1+X^p$. Multiply by $(1+X{)}^k$ and compare coefficients of $X^r$ for $r<p$; the $X^p$ term cannot contribute.

// Target: foundations-of-mathematics.bigb