proposition: Lemma compare_spec (m m':t elt)`{!Ok m, !Ok m'} : compare cmp m m' = list_compare (pair_compare K.compare cmp) (bindings m) (bindings m').
proof: Proof. apply compare_Lcmp. Qed.
imports: Coq(Bool Arith BinInt FunInd) Coq(Orders OrdersFacts OrdersLists) MMaps(Comparisons Interface OrdList)