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