proposition: Lemma for_all_exists: forall s, exists_ f s = negb (for_all (fun x =>negb (f x)) s).
proof: Proof. intros. rewrite for_all_b; auto. rewrite exists_b; auto. induction (elements s); simpl; auto. destruct (f a); simpl; auto. Qed.
imports: MSetProperties Zerob Sumbool Lia DecidableTypeEx