proposition: Lemma remove_id (m: t elt) x : remove x m == m <-> ~In x m.
proof: Proof. rewrite not_in_find. split. - intros H. rewrite <- (H x). apply remove_spec1. - intros H y. rewrite !remove_o. now destruct K.eq_dec as [<-|E]. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)