proposition: Lemma min_elt_Below m x e : min_elt m = Some (x,e) -> Below x (remove x m).
proof: Proof. unfold min_elt, Below; intros. rewrite remove_in_iff in H0; destruct H0. rewrite bindings_in_iff in H1. destruct H1. generalize (bindings_spec2' m). destruct (bindings m). try discriminate. destruct p; injection H; intros; subst. inversion_clear H1. red in H2; destruct H2; simpl in *; F.order. inversion_clear H4. rewrite (@InfA_alt _ eqke) in H3; eauto with *. apply (H3 (y,x0)); auto. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)