generalize indexing in lemmas for series

[t6s]

Motivation for this change

There are several lemmas for series stated with zero-based indexing
0 <= k < n and n <oo.
This PR generalizes them to m <= k < n and m <= n<oo.

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Reference: How to document

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels

[t6s]

Two lemmas for orderTypes are added in mathcomp_extra.v too.