proposition: Lemma add_add_2 (m: t elt) x x' e e' : ~K.eq x x' -> add x e (add x' e' m) == add x' e' (add x e m).
proof: Proof. intros H y. rewrite !add_o. do 2 destruct K.eq_dec; auto. elim H. now transitivity y. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)