proposition: Lemma FinEnum_eq_equiv : forall (x y : FinEnum), FinEnum_eq x y <-> msp_eq x y.
proof: Proof. unfold FinEnum_eq, msp_eq. split. - intros. split. apply Qle_refl. split. intros z H0. rewrite H in H0. intro abs. apply (abs z). split. exact H0. reflexivity. intros z H0. rewrite <- H in H0. intro abs. apply (abs z). split. exact H0. reflexivity. - split. + intros z H0. destruct H as [_ [H1 _]]. specialize (H1 x0 z). clear z. unfold existsC in H1. contradict H1; intros x1 [H1 H2]. unfold InFinEnumC, FinSubset_ball in H1. contradict H1; intros [t H1]. contradict H0. exists t. split. apply H1. rewrite H2. apply H1. + intros z H0. destruct H as [_ [_ H1]]. specialize (H1 x0 z). clear z. unfold existsC in H1. contradict H1; intros x1 [H1 H2]. unfold InFinEnumC, FinSubset_ball in H1. contradict H1; intros [t H1]. contradict H0. exists t. split. apply H1. rewrite H2. apply H1. 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