proposition: Lemma ball_closed : forall e (a b:X), (forall d, 0 < d -> ball (e + d) a b) -> ball e a b.
proof: Proof. apply (msp_closed (msp X)). Qed.
imports: Coq.QArith.QArith CoRN.algebra.RSetoid MathClasses.interfaces.canonical_names MathClasses.interfaces.abstract_algebra