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