proposition: Lemma compare_spec (m m' :t) : CompareSpec (eq m m') (lt m m') (lt m' m) (compare m m').
proof: Proof. apply (P.compare_spec' _). Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)