for k, n being Nat holds
( (n + k) choose k = 1 iff ( n = 0 or k = 0 ) )