fact: Fixpoint remove x m := match m with | Leaf => Leaf | Node l y d r h => match X.compare x y with | LT _ => bal (remove x l) y d r | EQ _ => merge l r | GT _ => bal l y d (remove x r) end end.
imports: FunInd FMapInterface FMapList ZArith Int