even at the level of pseudometrictype. The fact that there are not leads to such [lemmas](https://github.com/math-comp/analysis/blob/dfddc69294d3a53782aae8202855320ac347fe35/theories/topology.v#L3741), where the use of interior should not be necessary.
