proposition: Lemma cardinal_Empty : forall m : t elt, Empty m <-> cardinal m = 0.
proof: Proof. intros. rewrite cardinal_1, elements_Empty. destruct (elements m); intuition; discriminate. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface