fact: Fixpoint remove x m := match m with | Leaf _ => Leaf _ | Node h l y d r => match K.compare x y with | Eq => append l r | Lt => bal (remove x l) y d r | Gt => bal l y d (remove x r) end end.
imports: Coq(Bool PeanoNat BinInt FunInd Int) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)