fact: Definition partition f m := let (l1,l2) := partition_aux f m nil nil in (treeify l1, treeify l2).
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)