proposition: Lemma exists_mem_1: forall s, (forall x, mem x s=true->f x=false) -> exists_ f s=false.
proof: Proof. intros. rewrite for_all_exists; auto. rewrite for_all_mem_1;auto with bool. intros;generalize (H x H0);intros. rewrite negb_true_iff; auto. Qed.
imports: MSetProperties Zerob Sumbool Lia DecidableTypeEx