proposition: Lemma min_elt_Empty : forall m, min_elt m = None -> Empty m.
proof: Proof. intros. unfold min_elt in *. rewrite elements_Empty. destruct (elements m); auto. destruct p; simpl in *; discriminate. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface