for n, k being Nat st k <= n holds
n choose k <= n |^ k