proposition: Lemma remove_b m x y : mem y (remove x m) = negb (eqb x y) && mem y m.
proof: Proof. rewrite !mem_find_b, remove_o; unfold eqb. now destruct (K.eq_dec x y). Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)