proposition: Lemma partition_2 : forall (s : t) (f : elt -> bool), compat_bool E.eq f -> Equal (snd (partition f s)) (filter (fun x => negb (f x)) s).
proof: Proof. intros s f; unfold partition; case M.partition. intro p; case p; clear p; intros s1 s2 H C. generalize (H (compat_P_aux C)); clear H; intro H. assert (D : compat_bool E.eq (fun x => negb (f x))). { generalize C; unfold compat_bool, Proper, respectful; intros; apply (f_equal negb); auto. } simpl; unfold Equal; intuition. - apply filter_3; firstorder with bool. - elim (H2 a); intros. assert (In a s). { eapply filter_1; eauto. } elim H3; intros; auto. absurd (f a = true). + intro. generalize (filter_2 D H1). rewrite H7; intros H8; inversion H8. + exact (H0 a H6). Qed.
imports: FSetInterface