theorem Th8: :: HILB10_8:8

for n, m being Nat st m ^2 <= n holds
ex T being _Theta st n choose m = ((n |^ m) / (m !)) * (1 + (T * ((m ^2) / n)))