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