rm dep on topo and ereal from altreals

[affeldt-aist]

Motivation for this change

fixes #1352

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Reference: How to document

Reminder to reviewers

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

[proux01]

@sertel this breaks ssprove. Very likely, it was accidentaly depending on the useless dependency and you need to add From mathcomp Require Import ereal topology. (or one of them) to some of your files.

[proux01]

This was part of #1349 but we can indeed have it as a separate PR.