proposition: Lemma for_all_mem_4: forall s, for_all f s=false -> {x:elt | mem x s=true /\ f x=false}.
proof: Proof. intros. rewrite for_all_filter in H; auto. destruct (choose_mem_3 _ H) as (x,(H0,H1));intros. exists x. rewrite filter_b in H1; auto. elim (andb_prop _ _ H1). split;auto. rewrite <- negb_true_iff; auto. Qed.
imports: MSetProperties Zerob Sumbool Lia DecidableTypeEx