proposition: Lemma msp_eq_refl : forall {m:MetricSpace} (x : m), msp_eq x x.
proof: Proof. intros. apply (msp_refl (msp m) (Qle_refl 0)). Qed.
imports: Coq.QArith.QArith CoRN.algebra.RSetoid MathClasses.interfaces.canonical_names MathClasses.interfaces.abstract_algebra