proposition: Lemma compare_spec m1 m2 : compare m1 m2 = Lcmp (bindings m1) (bindings m2).
proof: Proof. unfold compare. rewrite <- list_ecompare_fst. f_equal. apply ecompare_spec. Qed.
imports: Coq(Bool PeanoNat BinPos Orders OrdersEx OrdersLists) MMaps(Utils Comparisons Interface)