fact: Definition compare_more x1 d1 (cont:enumeration -> comparison) e2 := match e2 with | End => Gt | More x2 d2 r2 e2 => lex (K.compare x1 x2) (lex (cmp d1 d2) (cont (cons r2 e2))) end.
imports: Coq(Bool Arith BinInt FunInd) Coq(Orders OrdersFacts OrdersLists) MMaps(Comparisons Interface OrdList)