for n, k being Nat st n >= k holds
Product ((n + 1) + (- (idseq k))) = (k !) * (n choose k)