proposition: Lemma add_remove_1 (m: t elt) x e : add x e (remove x m) == add x e m.
proof: Proof. intro y. rewrite !add_o, !remove_o. now destruct K.eq_dec. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)