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