( k = (n + k) - n & n + k >= n + 0 ) by XREAL_1:6;
then (n + k) choose n = ((n + k) !) / ((n !) * (k !)) by NEWTON:def 3;
hence ((n + k) !) / ((n !) * (k !)) is natural ; :: thesis: verum