tentative removal of Rint

[affeldt-aist]

Motivation for this change

@agontard : what do you think about this change?
We do not use it a lot in MathComp-Analysis per se, as a user, we'd like your opinion.

TODO: introduce "type of ring for which the property of being an integer is decidable" and refactor, even though we do not have a use for it now, this could be a useful addition to MathComp

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

[CohenCyril]

Hi, Rint was using classical logic to exhibit integers in any realFieldType, while Num.int requires Archimedeanity, therefore they are incomparable, and with this PR you eliminate expressivity -- albeit apparently not used according to the CI. The proper way to refactor this would be to introduce the "type of ring for which the property of being an integer is decidable".

[affeldt-aist]

Note that the "generalization" to realFieldType was carried out some time ago
ef24876#diff-db2a60c8905528789fdebb5e121d48be6e89590ae44cfcdd26e1b037660707e0

It was not there originally.

[affeldt-aist]

So, in other words, I do not think that it was meant to correspond the "type of ring for which the property of being an integer is decidable". Shall we however PR the latter to MathComp?