proposition: Lemma SubMetricSpace_apdiag_grzero : forall (X : CMetricSpace) (P : X -> CProp), apdiag_imp_grzero (SubPsMetricSpace P) (cms_d (c:=SubPsMetricSpace P)).
proof: Proof. intros X P. unfold apdiag_imp_grzero in |- *. intros x y. simpl in |- *. case x. case y. simpl in |- *. intros. apply ax_d_apdiag_imp_grzero. auto. Qed.
imports: CoRN.metrics.Prod_Sub CoRN.metrics.Equiv