proposition: Lemma add_filter_2 : forall s s' x, f x=false -> (Add x s s') -> filter f s [=] filter f s'.
proof: Proof. unfold Add, MP.Add, Equal; intros. repeat rewrite filter_iff; auto. rewrite H0; clear H0. assert (f a = true -> ~E.eq x a). - intros H0 H1. rewrite (Comp _ _ H1) in H. rewrite H in H0; discriminate. - tauto. Qed.
imports: FSetProperties Zerob Sumbool DecidableTypeEx