l + 0 < l + k by XREAL_1:6;
hence l choose (l + k) is zero by NEWTON:def 3; :: thesis: verum