proposition: Lemma split_in_l m x y `{!Ok m} : (y ∈ (split x m)#l <-> y ∈ m /\ y < x).
proof: Proof. functional induction (split x m); intros; cleansplit; rewrite ?join_in, ?IHt; intuition_in; order. Qed.
imports: Coq(Bool PeanoNat BinInt FunInd Int) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)