proposition: Lemma cardinal_inv_2 : forall s n, cardinal s = S n -> { x : elt | In x s }.
proof: Proof. intros; rewrite FM.cardinal_1 in H. generalize (elements_2 (s:=s)). destruct (elements s); try discriminate. exists e; auto with relations. Qed.
imports: MSetInterface PeanoNat DecidableTypeEx OrdersLists MSetFacts MSetDecide