proposition: Lemma min_elt_Empty m : min_elt m = None -> Empty m.
proof: Proof. intros. unfold min_elt in *. rewrite bindings_Empty. destruct (bindings m); auto. destruct p; simpl in *; discriminate. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)