proposition: Lemma AlmostInExists_weak : forall (e d:Q) x (s:FinEnum X), e < d -> FinSubset_ball e x s -> { y:X | In y s /\ ball d x y }.
proof: Proof. intros. destruct (AlmostInExists H H0) as [n H1]. pose proof (nth_error_In s n). destruct (nth_error s n) as [y|]. 2: contradiction. exists y. split. exact (H2 y eq_refl). exact H1. 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