proposition: Lemma remove_b : forall m x y, mem y (remove x m) = negb (eqb x y) && mem y m.
proof: Proof. intros; do 2 rewrite mem_find_b; rewrite remove_o; unfold eqb. destruct (eq_dec x y); auto. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface