proposition: Lemma compare_equiv cmp (m m':t elt) : isEq (compare cmp m m') = equal (fun e e' => isEq (cmp e e')) m m'.
proof: Proof. apply eq_true_iff_eq. rewrite equal_spec. rewrite isEq_spec, compare_Equiv. unfold Equivb, Equiv, Cmp. now setoid_rewrite isEq_spec. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)