proposition: Lemma split_in_o m x : (split x m)#o = find x m.
proof: Proof. functional induction (split x m); intros; cleansplit; auto. Qed.
imports: Coq(Bool PeanoNat BinInt FunInd Int) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)