proposition: Lemma exists_filter : forall s, exists_ f s=negb (is_empty (filter f s)).
proof: Proof. intros; apply bool_1; split; intros. - destruct (exists_2 Comp H) as (a,(Ha1,Ha2)). apply bool_6. red; intros; apply (@is_empty_2 _ H0 a); auto with set. - generalize (@choose_1 (filter f s)) (@choose_2 (filter f s)). destruct (choose (filter f s)). + intros H0 _; apply exists_1; auto. exists e; generalize (H0 e); rewrite filter_iff; auto. + intros _ H0. rewrite (is_empty_1 (H0 Logic.eq_refl)) in H; auto; discriminate. Qed.
imports: FSetProperties Zerob Sumbool DecidableTypeEx