proposition: Lemma zf_nis_CMetricSpace : forall X : CSetoid, {x : X | {y : X | x[#]y}} -> Not (apdiag_imp_grzero (zf_as_CPsMetricSpace X) (cms_d (c:=zf_as_CPsMetricSpace X))).
proof: Proof. intros X Z. red in |- *. intro H. set (H1 := Build_CMetricSpace (zf_as_CPsMetricSpace X) H) in *. set (H2 := d_CMetricSpace_apdiag_imp_grzero H1) in *. generalize H2. unfold H1 in |- *. simpl in |- *. unfold apdiag_imp_grzero in |- *. unfold Zero_fun in |- *. simpl in |- *. unfold zero_fun in |- *. elim Z. intros x Z1. elim Z1. intros y Z2. intros H3. set (H4 := H3 x y Z2) in *. set (H5 := less_irreflexive_unfolded IR [0] H4) in *. exact H5. Qed.
imports: CoRN.metrics.Prod_Sub CoRN.metrics.Equiv