proposition: Lemma FinEnum_located : locatedMetric FinEnum.
proof: Proof. intros e d a b Hed. destruct (Q.Qle_dec 0 e). - destruct (@HemiMetricStrongAlmostDecidable _ _ a b Hed). destruct (@HemiMetricStrongAlmostDecidable _ _ b a Hed). left. split. apply (Qle_trans _ _ _ q). apply Qlt_le_weak, Hed. split; assumption. right. intro abs. destruct abs, H0. contradiction. right. intro abs. destruct abs, H0. contradiction. - right. intro abs. destruct abs. contradiction. Defined.
imports: CoRN.model.totalorder.QposMinMax CoRN.metric2.Hausdorff CoRN.logic.Classic CoRN.stdlib_omissions.List CoRN.metric2.Classification CoRN.metric2.Complete CoRN.metric2.Prelength