proposition: Lemma for_all_filter: forall s, for_all f s=is_empty (filter (fun x => negb (f x)) s).
proof: Proof. intros; apply bool_1; split; intros. - apply is_empty_1. unfold Empty; intros. rewrite filter_iff; auto. red; destruct 1. rewrite <- (@for_all_iff s f) in H; auto. rewrite (H a H0) in H1; discriminate. - apply for_all_1; auto; red; intros. revert H; rewrite <- is_empty_iff. unfold Empty; intro H; generalize (H x); clear H. rewrite filter_iff; auto. destruct (f x); auto. Qed.
imports: MSetProperties Zerob Sumbool Lia DecidableTypeEx