fact: Fixpoint partition_aux f m acc1 acc2 := match m with | Leaf => (acc1,acc2) | Node _ l k v r => let (acc1, acc2) := partition_aux f r acc1 acc2 in if f k v then partition_aux f l ((k,v)::acc1) acc2 else partition_aux f l acc1 ((k,v)::acc2) end.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)