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 #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