proposition: Lemma InStrengthen : forall x (l:FinEnum Q2), InFinEnumC x l -> exists y : Q2, In y l /\ msp_eq x y.
proof: Proof. induction l. intro abs. exfalso; exact (FinSubset_ball_nil abs). intros H. assert (L:msp_eq x a \/ ~msp_eq x a). destruct (Qeq_dec (fst x) (fst a)). destruct (Qeq_dec (snd x) (snd a)). left. split; apply Qball_0; auto. right; intros [_ B]. apply Qball_0 in B. contradiction. right; intros [B _]. apply Qball_0 in B. contradiction. destruct L. exists a. split; auto with *. destruct (IHl) as [y [Hy0 Hy1]]. apply FinSubset_ball_orC in H. destruct H as [G | H | H] using orC_ind. intro abs. contradict G; intro G. contradiction. elim H0; auto. exact H. exists y. split; auto with *. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.raster.Raster CoRN.reals.fast.Interval CoRN.metric2.FinEnum CoRN.metric2.ProductMetric CoRN.logic.Classic