proposition: Lemma filter_add_2 : forall s x, f x = false -> filter f (add x s) [=] filter f s.
proof: Proof. red; intros; do 2 (rewrite filter_iff; auto); set_iff. intuition. assert (f x = f a) by (apply Comp; auto). rewrite H in H1; rewrite H2 in H1; discriminate. Qed.
imports: MSetProperties Zerob Sumbool Lia DecidableTypeEx