proposition: Lemma metric_ap_irreflexive : forall X : CPsMetricSpace, irreflexive (metric_ap X).
proof: Proof. intro X. unfold irreflexive in |- *. intro x. red in |- *. unfold metric_ap in |- *. set (H0 := pos_imp_ap_imp_diag_zero X (cms_d (c:=X)) (ax_d_pos_imp_ap X (cms_d (c:=X)) (CPsMetricSpace_is_CPsMetricSpace X)) (ax_d_nneg X (cms_d (c:=X)) (CPsMetricSpace_is_CPsMetricSpace X))) in *. generalize H0. unfold diag_zero in |- *. intros H1 H2. set (H3 := less_wdr IR [0] (x[-d]x) [0] H2 (H1 x)) in *. set (H4 := less_irreflexive_unfolded IR [0] H3) in *. exact H4. Qed.
imports: CoRN.metrics.Prod_Sub CoRN.metrics.Equiv