proposition: Lemma metric_ap_tight : forall X : CPsMetricSpace, tight_apart (metric_eq X) (metric_ap X).
proof: Proof. intro X. unfold tight_apart in |- *. unfold metric_ap in |- *. unfold metric_eq in |- *. intros x y. split. intro H. cut (ZeroR[<=]x[-d]y). rewrite -> leEq_def in |- *. intro H1. cut (Not (x[-d]y[#][0])). intro H2. apply not_ap_imp_eq. exact H2. red in |- *. intro H2. set (H3 := less_conf_ap IR (x[-d]y) [0]) in *. elim H3. intros H4 H5. set (H6 := H4 H2) in *. elim H6. intuition. intuition. apply ax_d_nneg. apply CPsMetricSpace_is_CPsMetricSpace. intro H. red in |- *. intro H0. set (H1 := less_wdr IR [0] (x[-d]y) [0] H0 H) in *. set (H2 := less_irreflexive_unfolded IR [0] H1) in *. exact H2. Qed.
imports: CoRN.metrics.Prod_Sub CoRN.metrics.Equiv