proposition: Lemma flatten_e_bindings : forall (l:t elt) r x d z e, bindings l ++ flatten_e (More x d r e) = bindings (Node z l x d r) ++ flatten_e e.
proof: Proof. intros. now rewrite bindings_node, <- app_assoc. Qed.
imports: Coq(Bool Arith BinInt FunInd) Coq(Orders OrdersFacts OrdersLists) MMaps(Comparisons Interface OrdList)