proposition: Lemma filter_add_1 : forall s x, f x = true -> filter f (add x s) [=] add x (filter f s).
proof: Proof. red; intros; set_iff; do 2 (rewrite filter_iff; auto); set_iff. intuition. rewrite <- H; apply Comp; auto. Qed.
imports: FSetProperties Zerob Sumbool DecidableTypeEx