consider m being Nat such that
A1: n ! = ((min (n,k)) !) * m by MDF1, NAT_D:def 3;
thus (n !) / ((min (n,k)) !) is natural by A1, XCMPLX_1:89; :: thesis: verum