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