Refactor metric spaces

[malarbol]

Refactoring the metric space module (#1421)

• remove the notion of Premetric / Premetric-Space:

  as we discussed, the term "premetric" has too many different meanings to be reliably used in this library. What was called a Premetric is now a Rational-Neighborhood-Relation and we only focus on (pseudo)metric spaces.

• all (pseudo)metric spaces are saturated:

  including saturation in the definition of pseudometric space is coherent with the definition of Richman premetric spaces and makes a lot of things easier (e.g.: the limit map is short, the metric space of Cauchy approximations in a complete metric space is complete, etc.).

• simplify hierarchy in concepts (define things for for metric spaces first, instead of the splitting premetric>pseudometric>metric):

  although a lot of concepts only depend on the underlying neighborhood relation, they are principally useful for (pseudo)metric spaces. We prioritized definitions on metric spaces, which is where they're the most useful; if we need the corresponding concepts for pseudometric spaces, we can add them later. (e.g. we'll probably want isometry-Pseudometric-Space at some point but I think this PR is already big enough).