proposition: Lemma singleton_cardinal : forall x, cardinal (singleton x) = 1.
proof: Proof. intros. rewrite (singleton_equal_add x). replace 0 with (cardinal empty); auto with set. apply cardinal_2 with x; auto with set. Qed.
imports: MSetInterface PeanoNat DecidableTypeEx OrdersLists MSetFacts MSetDecide