proposition: Lemma cardinal_inv_2 : forall m n, cardinal m = S n -> { p : key*elt | MapsTo (fst p) (snd p) m }.
proof: Proof. intros; rewrite M.cardinal_1 in *. generalize (elements_mapsto_iff m). destruct (elements m); try discriminate. exists p; auto. rewrite H0; destruct p; simpl; auto. constructor; red; auto. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface