proposition: Lemma prod_is_MetricSpace : is_MetricSpace prod_ball.
proof: Proof. split. - intros. intros a. apply prod_ball_refl, H. - exact prod_ball_sym. - exact prod_ball_triangle. - exact prod_ball_closed. - intros. destruct H. apply (msp_nonneg (msp X)) in H. exact H. - intros. split. + apply (msp_stable (msp X)). intro abs. contradict H; intros [H _]. contradiction. + apply (msp_stable (msp Y)). intro abs. contradict H; intros [_ H]. contradiction. Qed.
imports: CoRN.model.totalorder.QposMinMax CoRN.metric2.Metric CoRN.metric2.Classification CoRN.metric2.UniformContinuity CoRN.metric2.Prelength CoRN.metric2.Complete CoRN.metric2.LocatedSubset