proposition: Lemma is_CMetricSpace_diag_zero : forall (X : CSetoid) (d : CSetoid_bin_fun X X IR) (H : com d) (H1 : tri_ineq d) (H2 : nneg d) (H3 : diag_zero X d) (H4 : apdiag_imp_grzero X d), CMetricSpace.
proof: Proof. intros X d H H1 H2 H3 H4. set (H5 := Build_is_CPsMetricSpace X d H H2 (diag_zero_imp_pos_imp_ap X d H3) H1) in *. set (H6 := Build_CPsMetricSpace X d H5) in *. set (H7 := Build_CMetricSpace H6 H4) in *. exact H7. Qed.
imports: CoRN.metrics.Prod_Sub CoRN.metrics.Equiv