fact: Definition RemoveMin m res := match m with | Leaf _ => False | Node h l x e r => remove_min l x e r = res end.
imports: Coq(Bool PeanoNat BinInt FunInd Int) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)