let n be Nat; :: thesis: (2 * n) choose n = ((2 * n) !) / ((n !) |^ 2)
A1: n = (2 * n) - n ;
n + n >= n + 0 by XREAL_1:6;
then (2 * n) choose n = ((2 * n) !) / ((n !) * (n !)) by A1, NEWTON:def 3;
hence (2 * n) choose n = ((2 * n) !) / ((n !) |^ 2) by NEWTON:81; :: thesis: verum