fact: Fixpoint partition (f:key->elt->bool) m := match m with | Leaf _ => (Leaf _, Leaf _) | Node _ l x e r => let '(l1,l2) := partition f l in let '(r1,r2) := partition f r in if f x e then (join l1 x e r1, concat l2 r2) else (concat l1 r1, join l2 x e r2) end.
imports: Coq(Bool PeanoNat BinInt FunInd Int) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)