fact: Record is_DistanceMetricSpace (X : RSetoid) (distance: X -> X -> CR) : Prop := Build_is_DistanceMetricSpace { dmsp_refl: forall x y, st_eq x y <-> distance x y == 0 ; dmsp_sym: forall x y, distance x y == distance y x ; dmsp_triangle: forall x y z, distance x z <= distance x y + distance y z ; dmsp_nonneg: forall x y, 0 <= distance x y }.
imports: CoRN.algebra.RSetoid CoRN.model.totalorder.QposMinMax CoRN.metric2.Metric CoRN.reals.fast.CRArith