proposition: Lemma add_above_bindings x e m : m < x -> bindings (add x e m) = bindings m ++ (x,e) :: nil.
proof: Proof. functional induction (add x e m); simpl; intros; cleanf; trivial; invlt; try (intuition; order). rewrite bal_bindings. unfold create. rewrite !bindings_node. rewrite <- app_assoc. f_equal. simpl. f_equal. intuition. Qed.
imports: Coq(Bool PeanoNat BinInt FunInd Int) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)