proposition: Lemma add_add_1 (m: t elt) x e : add x e (add x e m) == add x e m.
proof: Proof. intros y. rewrite !add_o. destruct K.eq_dec; auto. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)