proposition: Lemma is_MetricSpace: is_MetricSpace ball.
proof: Proof. Proof with auto. constructor. - apply ball_refl. - apply ball_sym. - apply ball_triangle. - apply ball_closed. - intros. destruct H. exact H. - unfold ball. split. destruct (Qlt_le_dec e 0). exfalso. contradict H; intros [H _]. exact (Qlt_not_le _ _ q H). exact q. apply CRle_not_lt. intro abs. contradict H; intros [_ H]. revert abs. apply CRle_not_lt, H. Qed.
imports: CoRN.algebra.RSetoid CoRN.model.totalorder.QposMinMax CoRN.metric2.Metric CoRN.reals.fast.CRArith