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