proposition: Lemma AlmostInExists : forall (e d:Q) x (s:FinEnum X), e < d -> FinSubset_ball e x s -> { n:nat | match nth_error s n with | None => False | Some y => ball d x y end }.
proof: Proof. intros e d x s Hed. induction s. intro abs; exfalso; exact (FinSubset_ball_nil abs). intros H. destruct (@locatedX _ _ x a Hed) as [close|far]. exists O. exact close. destruct IHs as [n Hy]. abstract (intros H0; apply FinSubset_ball_orC in H; apply H; split; auto). exists (S n). exact Hy. Defined.
imports: CoRN.model.totalorder.QposMinMax CoRN.metric2.Limit CoRN.metric2.FinEnum Coq.ZArith.Zpow_facts CoRN.metric2.Complete CoRN.logic.Classic Coq.QArith.Qpower Coq.QArith.Qround