proposition: Lemma max_elt_MapsTo : forall m x e, max_elt m = Some (x,e) -> MapsTo x e m.
proof: Proof. intros. unfold max_elt in *. rewrite elements_mapsto_iff. induction (elements m). - simpl; try discriminate. - destruct a; destruct l; simpl in *. + injection H; intros; subst; constructor; red; auto with ordered_type. + constructor 2; auto. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface