proposition: Lemma ball_eq : forall (a b:X), (forall e, 0 < e -> ball e a b) -> msp_eq a b.
proof: Proof. intros. apply ball_closed. intros. rewrite Qplus_0_l. apply H, H0. Qed.
imports: Coq.QArith.QArith CoRN.algebra.RSetoid MathClasses.interfaces.canonical_names MathClasses.interfaces.abstract_algebra