proposition: Lemma remove_b : mem y (remove x s) = mem y s && negb (eqb x y).
proof: Proof. generalize (mem_iff (remove x s) y)(mem_iff s y)(remove_iff s x y); unfold eqb. destruct (eq_dec x y); destruct (mem y s); destruct (mem y (remove x s)); simpl; intuition. Qed.
imports: DecidableTypeEx MSetInterface