fact: Fixpoint max_binding (t : tree) : option (key * elt) := match t with | Leaf => None | Node _ l x e Leaf => Some (x,e) | Node _ l x e r => max_binding r end.
imports: Coq(Bool Arith BinInt FunInd) Coq(Orders OrdersFacts OrdersLists) MMaps(Comparisons Interface OrdList)