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