proposition: Lemma CPsMetricSpace_is_CPsMetricSpace : is_CPsMetricSpace A cms_d.
proof: Proof. Proof cms_proof A. Lemma d_com : com (cms_d (c:=A)). Proof. elim CPsMetricSpace_is_CPsMetricSpace. auto. Qed.
imports: CoRN.reals.Intervals