proposition: Lemma Ens_to_FSet : forall e : Ensemble M.elt, Finite _ e -> exists s:M.t, !!s === e.
proof: Proof. induction 1. - exists M.empty. apply empty_Empty_Set. - destruct IHFinite as (s,Hs). exists (M.add x s). apply Extensionality_Ensembles in Hs. rewrite <- Hs. apply add_Add. Qed.
imports: Ensembles Finite_sets FSetInterface FSetProperties OrderedTypeEx DecidableTypeEx