for n, m being Nat st m >= 1 holds
n + 1 <= (n + m) choose m