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