proposition: Lemma max_elt_Empty : forall m, max_elt m = None -> Empty m.
proof: Proof. intros. unfold max_elt in *. rewrite elements_Empty. induction (elements m); auto. destruct a; destruct l; simpl in *; try discriminate. assert (H':=IHl H); discriminate. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface