fact: Definition gtb (p p':key*elt) := match K.compare (fst p) (fst p') with Gt => true | _ => false end.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)