fact: Record DistanceMetricSpace: Type := Build_alt_MetricSpace { dmsp_is_setoid:> RSetoid; distance: dmsp_is_setoid -> dmsp_is_setoid -> CR; distance_wd: Proper (@st_eq _ ==> @st_eq _ ==> @msp_eq _) distance; dmsp : is_DistanceMetricSpace dmsp_is_setoid distance }.
imports: CoRN.algebra.RSetoid CoRN.model.totalorder.QposMinMax CoRN.metric2.Metric CoRN.reals.fast.CRArith