proposition: Lemma cardinal_inv_2b : forall m, cardinal m <> 0 -> { p : key*elt | MapsTo (fst p) (snd p) m }.
proof: Proof. intros. generalize (@cardinal_inv_2 m); destruct cardinal. - elim H;auto. - eauto. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface