proposition: Lemma FinSubset_ball_nonneg : forall (e:Q) x l, FinSubset_ball e x l -> 0 <= e.
proof: Proof. intros. apply Qnot_lt_le. intro abs. unfold FinSubset_ball in H. contradict H; intros [y [_ H]]. apply (Qlt_not_le _ _ abs). apply (msp_nonneg (msp X) e x y H). Qed.
imports: CoRN.model.totalorder.QposMinMax CoRN.metric2.Hausdorff CoRN.logic.Classic CoRN.stdlib_omissions.List CoRN.metric2.Classification CoRN.metric2.Complete CoRN.metric2.Prelength