proposition: Lemma msp_eq_trans : forall {m:MetricSpace} (x y z : m), msp_eq x y -> msp_eq y z -> msp_eq x z.
proof: Proof. unfold msp_eq. intros. rewrite <- (ball_wd m (Qplus_0_r 0) x x (msp_eq_refl x) z z (msp_eq_refl z)). exact (msp_triangle (msp m) _ _ _ y _ H H0). Qed.
imports: Coq.QArith.QArith CoRN.algebra.RSetoid MathClasses.interfaces.canonical_names MathClasses.interfaces.abstract_algebra