mv squeeze for R earlier

[affeldt-aist]

Motivation for this change

This PR is essentially moving squeeze_cvgr from normed_module.v to the topology_theory directory
so that it is available to develop the theory of TVSs.

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]

CI green (fyi: @mkerjean )

[mkerjean]

Looks great, thanks. As the CI is green it can be merged. Could you explain why the necessity to duplicate cvgrPdistC_lt or cvgr_distC_lt ? Would solving it necessitate the creation of a pseudometric type?

[affeldt-aist]

Looks great, thanks. As the CI is green it can be merged. Could you explain why the necessity to duplicate cvgrPdistC_lt or cvgr_distC_lt ?

By putting a Let here, I can prove the needed lemma with a minimal assumption (R : numFieldType)
and I do not commit to anything (it is a Let, it can't be used outside).
If I were to put cvgrPdistC_lt in the module metricType_numDomainType along with other generalizations
(generalizations from normed modules to metric space, WIP),
I would need R : realFieldType to be able to use mdist x y = mdist y x,
which would cause the section (with the lemmas real_cvgr_lt, etc.) to require R : realFieldType instead of numFieldType, which would be a regression compared with the current state of MathComp-Analysis.

So this is really just a way to make an incremental progress (put the squeeze theorem in the right place and
move a minimal set of lemmas without losing "generality") and defer big changes (generalization of more lemmas
to metric spaces) to later.

Would solving it necessitate the creation of a pseudometric type?

Sorry, I can't see it. Which type are you thinking of? Pseudometric in the MCA sense or in the sense "d(x,y)=0 does not necessarily imply x=y"? In the latter case, it does not seem to be the incriminating property, that's why I can't see how it would help right away.