let k, n be Nat; :: thesis: (k + n) choose n = (k + n) choose k
( (k + n) - k = n & k + n >= k + 0 ) by XREAL_1:6;
hence (k + n) choose n = (k + n) choose k by NEWTON:20; :: thesis: verum