fact: Fixpoint maxdepth s := match s with | Leaf => 0 | Node _ l _ _ r => S (max (maxdepth l) (maxdepth r)) end.
imports: Coq(Bool Arith BinInt FunInd) Coq(Orders OrdersFacts OrdersLists) MMaps(Comparisons Interface OrdList)