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