normed module identity convergence lemmas

[amolinamounier]

Motivation for this change

Split from #2023. Adds convenient cvg lemmas that involves the additive and multiplicative identities of normed modules.

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Reference: How to document

Merge policy

As a rule of thumb:

• PRs with several commits that make sense individually and that
  all compile are preferentially merged into master.
• PRs with disorganized commits are very likely to be squash-rebased.

Reminder to reviewers

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

[affeldt-aist]

What about cvgcstD to suggest that the constant is on the left (and cvgDcst instead of cvgDr)?
Because cvgDl does not really say what is on the left.

But in fact I am not sure that cvgDl, cvgDr, cvgBl, cvgBr are very useful,
because it is just cvg{D,B} with cvg_cst.
The application of cvg_cst should maybe be automatic instead
(and maybe it was thought as such because there is actually a Hint in topology_structure.v but it is not working here). Fixing the latter Hint could be better.

[amolinamounier]

Yes, I think that would be a better idea; I did find it a bit odd that cvg_cst didn't trigger automatically.

[affeldt-aist]

Trying to fix that: #2046

[affeldt-aist]

So now cvg_cst and is_cvg_cst are true hints, this PR can maybe be simplified.

[affeldt-aist]

I have added cvgZ variants and tried to find a handful of places in the code where the new lemmas can actually be used. Since cvg_cst is now a proper hint, I am not sure that the cst variants are still useful. I tentatively removed them. If you are fine with that change, I think that we can merge. Note that we can always reintroduce the cst versions later if really needed.

[amolinamounier]

I generalized the lemmas to be in line with the others, and added a cvgZ0 lemma. If there was a file for normed algebras I would have added a cvgZ1 as well.