proposition: Lemma split_lt_r m x y : m < y -> (split x m)#r < y.
proof: Proof. intros ? z Hz. apply split_in_r0 in Hz. order. Qed.
imports: Coq(Bool PeanoNat BinInt FunInd Int) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)