proposition: Lemma max_elt_MapsTo m x e : max_elt m = Some (x,e) -> MapsTo x e m.
proof: Proof. intros. unfold max_elt in *. rewrite bindings_mapsto_iff. induction (bindings m); simpl; try easy. rewrite InA_cons. destruct a; destruct l; simpl in *. injection H as -> ->. now left. right; auto. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)