proposition: Lemma ball_stable : forall e (x y : X), ~~(ball e x y) -> ball e x y.
proof: Proof. intros. apply (msp_stable (msp X)), H. Qed.
imports: Coq.QArith.QArith CoRN.algebra.RSetoid MathClasses.interfaces.canonical_names MathClasses.interfaces.abstract_algebra