proposition: Lemma ball_triangle : forall e1 e2 (a b c:X), ball e1 a b -> ball e2 b c -> ball (e1 + e2) a c.
proof: Proof. apply (msp_triangle (msp X)). Qed.
imports: Coq.QArith.QArith CoRN.algebra.RSetoid MathClasses.interfaces.canonical_names MathClasses.interfaces.abstract_algebra