proposition: Lemma compare_spec' m m' : CompareSpec (eq m m') (lt m m') (lt m' m) (compare cmp m m').
proof: Proof. unfold eq, lt. rewrite (@sym _ (compare cmp) _ m m'). destruct (compare cmp m m'); auto. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)