proposition: Lemma partition_1 : forall (s : t) (f : elt -> bool), compat_bool E.eq f -> Equal (fst (partition f s)) (filter f 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. simpl; unfold Equal; intuition. - apply filter_3; firstorder. - elim (H2 a); intros. assert (In a s). + eapply filter_1; eauto. + elim H3; intros; auto. absurd (f a = true). * exact (H a H6). * eapply filter_2; eauto. Qed.
imports: FSetInterface