theorem Th12: :: RAMSEY_1:12
for n, m being Nat st m >= 1 & n >= 1 holds
m + 1 <= (n + m) choose m