proposition: Lemma msp_eq_sym : forall {m:MetricSpace} (x y : m), msp_eq x y -> msp_eq y x.
proof: Proof. intros. apply (msp_sym (msp m)), H. Qed.
imports: Coq.QArith.QArith CoRN.algebra.RSetoid MathClasses.interfaces.canonical_names MathClasses.interfaces.abstract_algebra