for n, k being Nat holds (n !) / ((n -' k) !) is Element of NAT