proposition: Lemma uc_is_MetricSpace : is_MetricSpace ucBall.
proof: Proof. constructor. - firstorder using ball_refl. - firstorder using ball_sym. - intros e1 e2 f g h H1 H2. destruct H1, H2. split. apply (Qle_trans _ (e1+0)). rewrite Qplus_0_r. exact H. apply Qplus_le_r, H1. intro a. apply ball_triangle with (g a); auto. - intros e f g H. split. + apply Qnot_lt_le. intro abs. specialize (H (-e *(1#2))). destruct H. rewrite <- (Qmult_0_l (1#2)). apply Qmult_lt_r. reflexivity. apply (Qplus_lt_r _ _ e). ring_simplify. exact abs. ring_simplify in H. apply (Qlt_not_le _ _ abs). rewrite <- (Qmult_le_l _ _ (1#2)). rewrite Qmult_0_r. exact H. reflexivity. + intro a. apply ball_closed. firstorder. - intros e a b H. apply H. - intros. split. apply Qnot_lt_le. intro abs. contradict H; intro H. destruct H. apply (Qle_not_lt _ _ H abs). intros. apply (msp_stable (msp Y)). intro abs. contradict H; intro H. apply abs, H. Qed.
imports: CoRN.model.totalorder.QposMinMax CoRN.metric2.Metric CoRN.model.structures.QposInf CoRN.stdlib_omissions.List