I am surprised that it is sufficient to have an ordered-ring valued metric to get a topology. Why not a (nontrivial) linearly ordered group then? I think you can show metric_positive without using the unit, same with balls_coverS. Am I missing something?