for i, j, n being Nat st i <= j & 2 * j <= n + 1 holds
n choose i <= n choose j