proposition: Lemma cardinal_inv_2b : forall s, cardinal s <> 0 -> { x : elt | In x s }.
proof: Proof. intro; generalize (@cardinal_inv_2 s); destruct cardinal; [intuition|eauto]. Qed.
imports: MSetInterface PeanoNat DecidableTypeEx OrdersLists MSetFacts MSetDecide