proposition: Lemma ball_refl : forall e (a:X), 0 <= e -> ball e a a.
proof: Proof. intros. apply (msp_refl (msp X) H). Qed.
imports: Coq.QArith.QArith CoRN.algebra.RSetoid MathClasses.interfaces.canonical_names MathClasses.interfaces.abstract_algebra