proposition: Lemma bindings_split : forall p m, bindings m = bindings_lt p m ++ bindings_ge p m.
proof: Proof. unfold bindings_lt, bindings_ge, leb; intros. apply filter_split with (eqA:=eqk) (ltA:=ltk); eauto with *. intros; destruct x; destruct y; destruct p. rewrite gtb_1 in H; klean. apply not_true_iff_false in H0. rewrite gtb_1 in H0. klean. F.order. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)