for k, n being Nat st k <= n holds
(n !) / (k !) is integer