proposition: Lemma max_elt_Empty m : max_elt m = None -> Empty m.
proof: Proof. intros. unfold max_elt in *. rewrite bindings_Empty. induction (bindings m); auto. destruct a; destruct l; simpl in *; try discriminate. assert (H':=IHl H); discriminate. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)