fact: Definition msp_as_RSetoid : MetricSpace -> RSetoid := fun m => Build_RSetoid (msp_Setoid m).
imports: Coq.QArith.QArith CoRN.algebra.RSetoid MathClasses.interfaces.canonical_names MathClasses.interfaces.abstract_algebra