proposition: Lemma FinEnum_eq_rev : forall X (f:FinEnum X), msp_eq f (rev f).
proof: Proof. intros. apply FinEnum_eq_equiv. split. - intros H abs. unfold InFinEnumC, FinSubset_ball in H. contradict H; intros [y H]. contradict abs. exists y. split. rewrite <- in_rev. apply H. apply H. - intros H abs. unfold InFinEnumC, FinSubset_ball in H. contradict H; intros [y H]. contradict abs. exists y. split. rewrite in_rev. apply H. apply H. 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