proposition: Lemma bal_find l x e r y `{!Ok l, !Ok r} : l < x -> x < r -> find y (bal l x e r) = find y (create l x e r).
proof: Proof. functional induction (bal l x e r); intros; cleanf; trivial; invok; invlt; simpl; repeat case K.compare_spec; intuition; order. Qed.
imports: Coq(Bool PeanoNat BinInt FunInd Int) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)