theorem Th4: :: NAT_4:4

for n, k, m being Nat st k <= n & m = [\(n / 2)/] holds
n choose m >= n choose k