proposition: Lemma ball_sym : forall e (a b:X), ball e a b -> ball e b a.
proof: Proof. apply (msp_sym (msp X)). Qed.
imports: Coq.QArith.QArith CoRN.algebra.RSetoid MathClasses.interfaces.canonical_names MathClasses.interfaces.abstract_algebra