theorem :: GROUP_10:15

for n, m, r being Nat
for p being Prime st n = (p |^ r) * m & not p divides m holds
(n choose (p |^ r)) mod p <> 0 by Lm5;