( len (Newton_Coeff l) = l + 1 & (l + 1) + 0 < (l + 1) + k ) by XREAL_1:6, NEWTON:def 5;
hence (Newton_Coeff l) . ((l + k) + 1) is zero ; :: thesis: verum