proposition: Lemma compare_refl m : compare cmp m m = Eq.
proof: Proof. destruct (compare cmp m m) eqn:E; auto; assert (E':=E). rewrite sym, CompOpp_iff in E. simpl in E. congruence. rewrite sym, CompOpp_iff in E. simpl in E. congruence. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)