for n, k being Nat st k <= n holds
n ! <= (k !) * (n |^ (n -' k))