reconsider m = min (n,k) as Nat ;
( n >= m & k >= m ) by XXREAL_0:17;
then n + k >= m + m by XREAL_1:7;
then (n + k) - (2 * m) >= (2 * m) - (2 * m) by XREAL_1:9;
then reconsider d = (n + k) - (2 * m) as Nat ;
A0: (((2 * m) !) / ((m !) |^ 2)) * ((m !) |^ 2) = (2 * m) ! by XCMPLX_1:87;
A1: (2 * m) ! divides ((2 * m) + d) ! by MDF;
((m + m) !) / ((m !) * (m !)) is natural ;
then ((2 * m) !) / ((m !) |^ 2) is natural by NEWTON:81;
then (m !) |^ 2 divides (2 * m) ! by A0;
then consider a being Nat such that
A2: ((2 * m) + d) ! = ((m !) |^ 2) * a by A1, INT_2:9, NAT_D:def 3;
thus ((n + k) !) / (((min (n,k)) !) |^ 2) is natural by A2, XCMPLX_1:89; :: thesis: verum