proposition: Lemma compare_Lcmp m1 m2 : compare cmp m1 m2 = Lcmp (bindings m1) (bindings m2).
proof: Proof. unfold compare; simpl. rewrite <- (app_nil_r (bindings m1)). replace (bindings m2) with (flatten_e (cons m2 (End _))) by (rewrite cons_1; simpl; rewrite app_nil_r; auto). apply compare_cont_Lcmp. now destruct e. Qed.
imports: Coq(Bool Arith BinInt FunInd) Coq(Orders OrdersFacts OrdersLists) MMaps(Comparisons Interface OrdList)