proposition: Lemma max_elt_Above m x e : max_elt m = Some (x,e) -> Above x (remove x m).
proof: Proof. red; intros. rewrite remove_in_iff in H0. destruct H0. rewrite bindings_in_iff in H1. destruct H1. unfold max_elt in *. generalize (bindings_spec2' m). revert x e H y x0 H0 H1. induction (bindings m); try easy. intros. destruct a; destruct l; simpl in *. - injection H; clear H; intros; subst. inversion_clear H1. + compute in H; simpl in *; intuition. order. + inversion H. - change (optlast (p::l) = Some (x,e)) in H. generalize (IHl x e H); clear IHl; intros IHl. inversion_clear H1; [ | inversion_clear H2; eauto ]. compute in H3; destruct H3. subst. destruct p as (p1,p2). destruct (K.eq_dec p1 x) as [Heq|Hneq]. + rewrite <- Heq; auto. inversion_clear H2. inversion_clear H4. compute in H2; F.order. + transitivity p1; auto. * inversion_clear H2. inversion_clear H4. compute in H2; F.order. * inversion H2; subst. eapply IHl; eauto with *. econstructor; eauto. compute; eauto with *. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)