proposition: Lemma cardinal_Empty : forall s, Empty s <-> cardinal s = 0.
proof: Proof. intros. rewrite elements_Empty, M.cardinal_1. destruct (elements s); intuition; discriminate. Qed.
imports: FSetInterface PeanoNat DecidableTypeEx FSetFacts FSetDecide