Splitting proofs and reshuffling code

[CohenCyril]

Motivation for this change

This PR slightly refactor the proof of topolology for \bar R, for R : realFieldType and exhibitting the wrong behaviour for R : numFieldType.

@affeldt-aist This PR also provide the proof in https://github.com/math-comp/analysis/pull/1040 but without the dependency in C... (thus assuming the existence of i st `|i| = 1 and i \isn't Num.real).

Things done/to do

• [ ] added corresponding entries in CHANGELOG_UNRELEASED.md

• ~~added corresponding documentation in the headers~~

Compatibility with MathComp 2.0

• [ ] I added the label TODO: HB port to make sure someone ports this PR to the hierarchy-builder branch or I already opened an issue or PR (please cross reference).

Automatic note to reviewers

Read this Checklist and put a milestone if possible.

[affeldt-aist]

Thanks. This also makes (minor) generalizations clearer. While playing around with the topological definitions, I also observed the following one: issue #1042 now PRed in PR #1043