factory for hausdorff + pseudometric => metric

[affeldt-aist]

@zstone1 remarked in the conversion about PR #1589 (now merged)
that this factory will improve the code at several places:

"I'll note that there are a handful of places (itll take me a minute to find them all) where we use pseudometric + hausdorff instead of this. Might be nice for a followup PR to add a factory for hausdorff + pseudometric => metric too, and upgrade those places."

link to comment:
#1589 (comment)

[affeldt-aist]

@zstone1
We are trying to address this issue (@mkerjean).

Were you thinking about a factory along the lines of
https://github.com/affeldt-aist/analysis/blob/1d6572b7d81e51d8cfe7cca4b8923b177f2edcc3/theories/topology_theory/metric_structure.v#L347-L349
?

With this inferface, we failed to show that the following "distance":

Definition d (x y : M) := inf [set e : R | 0 < e /\ ball x e y].

indeed satisfies the last axiom of the metric mixin:

Let ballEd (x : M) delta : ball x delta = [set y | d x y < delta].

The problem seems to be that ball from pseudometric is not necessarily
open while the strict inequality enforces so.

How did you solve this conundrum in the code?
(It is maybe not edist in urysohn.v since balls are clopen there.)

PS: There is no hurry, we are just triaging issues.