proposition: Lemma zero (x y: M): msp_eq x y <-> CRball 0 x y.
proof: Proof. Proof with auto. split. intros H z zpos. apply (@ball_weak_le _ 0). apply CRle_Qle, zpos. exact H. intros. apply H. apply CRle_refl. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity Coq.QArith.Qabs CoRN.reals.fast.CRArith CoRN.reals.fast.CRabs