https://github.com/math-comp/analysis/blob/7622cc7f7392b8866d7900ffb6ab6b1e48e81a7f/theories/sequences.v#L1706 Following issue https://github.com/math-comp/analysis/issues/938 this maybe should be renamed `nneseriesZl`, and maybe also generalized to `\sum_(N <= n <oo)` from `\sum_(n <oo)`.
