fact: Definition min_elt m : option (key*elt) := match bindings m with | nil => None | (x,e)::_ => Some (x,e) end.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)