let k, n be Nat; :: thesis: ( (n + k) choose k = 1 iff ( n = 0 or k = 0 ) )
A1: ( n <> 0 & k <> 0 implies (n + k) choose k <> 1 )

proof

assume ( n <> 0 & k <> 0 ) ; :: thesis: (n + k) choose k <> 1
then reconsider m = n - 1, l = k - 1 as Nat ;
( (m + k) choose k >= 1 & (n + l) choose l >= 1 ) by NAT_1:14;
then B2: ((k + m) choose k) + ((l + n) choose l) >= 1 + 1 by XREAL_1:7;
((m + k) + 1) choose (l + 1) = ((m + k) choose k) + ((n + l) choose l) by NEWTON:22;
hence (n + k) choose k <> 1 by B2; :: thesis: verum

end;

( ( n = 0 or k = 0 ) implies (n + k) choose (k * 1) = 1 ) ;
hence ( (n + k) choose k = 1 iff ( n = 0 or k = 0 ) ) by A1; :: thesis: verum