proposition: Lemma is_CPsMetricSpace_diag_zero : forall (X : CSetoid) (d : CSetoid_bin_fun X X IR), com d /\ tri_ineq d /\ nneg d /\ diag_zero X d -> is_CPsMetricSpace X d.
proof: Proof. intros X d H. elim H. intros H1 H2. elim H2. intros H3 H4. elim H4. intros H5 H6. apply (Build_is_CPsMetricSpace X d H1 H5 (diag_zero_imp_pos_imp_ap X d H6) H3). Qed.
imports: CoRN.reals.Intervals