proposition: Lemma InFinEnumC_Qepsilon : forall (x y : Q) points, @InFinEnumC (ProductMS _ _) (x,y) points -> exists q, In q points /\ msp_eq q (x,y).
proof: Proof. intros. induction points as [|[i j] points]. - exfalso. unfold InFinEnumC, FinSubset_ball in H. contradict H; intros [z [H _]]. inversion H. - destruct (Qeq_dec x i). + destruct (Qeq_dec y j). exists (i,j). split. left. reflexivity. split; apply Qball_0; symmetry; assumption. destruct IHpoints. intro abs. unfold InFinEnumC, FinSubset_ball in H. contradict H; intros [z [zin H0]]. destruct zin. subst z. destruct H0. simpl in H0. apply Qball_0 in H0. contradiction. contradict abs. exists z. split. exact H. exact H0. exists x0. split. right. apply H0. apply H0. + destruct IHpoints. intro abs. unfold InFinEnumC, FinSubset_ball in H. contradict H; intros [z [zin H0]]. destruct zin. subst z. destruct H0. simpl in H. apply Qball_0 in H. contradiction. contradict abs. exists z. split. exact H. exact H0. exists x0. split. right. apply H0. apply H0. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.fast.RasterQ CoRN.reals.fast.Interval CoRN.logic.Classic CoRN.model.totalorder.QposMinMax Coq.QArith.Qabs Coq.QArith.Qround