mathlib documentation

data.nat.choose.dvd

Divisibility properties of binomial coefficients

theorem nat.prime.dvd_choose_add {p a b : } :
a < pb < pp a + bnat.prime pp (a + b).choose a

theorem nat.prime.dvd_choose_self {p k : } :
0 < kk < pnat.prime pp p.choose k