for n, k being Nat st n is prime & k <> 0 & k <> n holds
n divides n choose k