theorem :: NEWTON04:76

for n being Nat holds (2 * n) choose n = ((2 * n) !) / ((n !) |^ 2)