fact: Record MetricSpace : Type := { msp_car :> Type ; ball : Q -> msp_car -> msp_car -> Prop ; ball_e_wd : forall (e d : Q) (x y : msp_car), e == d -> (ball e x y <-> ball d x y) ; msp : is_MetricSpace ball }.
imports: Coq.QArith.QArith CoRN.algebra.RSetoid MathClasses.interfaces.canonical_names MathClasses.interfaces.abstract_algebra