reconsider n = l + k as Nat ;
( l = n - k & n >= k ) by NAT_1:11;
then n choose k = (n !) / ((k !) * (l !)) by NEWTON:def 3;
hence (l + k) choose k is positive ; :: thesis: verum