proposition: Lemma split_lt_l m x `{!Ok m} : (split x m)#l < x.
proof: Proof. intro. rewrite split_in_l; intuition; order. Qed.
imports: Coq(Bool PeanoNat BinInt FunInd Int) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)