proposition: Lemma Prod0CMetricSpaces_apdiag_grzero : forall X Y : CMetricSpace, apdiag_imp_grzero (Prod0CPsMetricSpace X Y) (cms_d (c:=Prod0CPsMetricSpace X Y)).
proof: Proof. intros X Y. unfold apdiag_imp_grzero in |- *. intros x y. case x. case y. intros c c0 c1 c2. simpl in |- *. intro H. elim H. intro H1. apply plus_resp_pos_nonneg. apply ax_d_apdiag_imp_grzero. exact H1. apply ax_d_nneg. apply CPsMetricSpace_is_CPsMetricSpace. intro H1. astepr ((c2[-d]c0)[+](c1[-d]c)). apply plus_resp_pos_nonneg. apply ax_d_apdiag_imp_grzero. exact H1. apply ax_d_nneg. apply CPsMetricSpace_is_CPsMetricSpace. Qed.
imports: CoRN.metrics.Prod_Sub CoRN.metrics.Equiv