proposition: Lemma ball_eq x y: (forall e, Qlt 0 e -> ball e x y) -> st_eq x y.
proof: Proof. unfold ball. intros. apply distance_refl. apply CRle_antisym. split. 2: apply (dmsp_nonneg _ _ (dmsp X)). apply CRle_not_lt. intro abs. apply CRlt_Qmid in abs. destruct abs as [q [H1 H2]]. apply Qlt_from_CRlt in H1. specialize (H q H1) as [_ H]. revert H2. apply CRle_not_lt, H. Qed.
imports: CoRN.algebra.RSetoid CoRN.model.totalorder.QposMinMax CoRN.metric2.Metric CoRN.reals.fast.CRArith