proposition: Lemma partition_spec1 : forall (s : t) (f : elt -> bool), Proper (X.eq==>eq) f -> Equal (fst (partition f s)) (filter f s).
proof: Proof. simple induction s; simpl; auto; unfold Equal. - split; auto. - intros x l Hrec f Hf. generalize (Hrec f Hf); clear Hrec. destruct (partition f l) as [s1 s2]; simpl; intros. case (f x); simpl; auto. split; inversion_clear 1; auto. + constructor 2; rewrite <- H; auto. + constructor 2; rewrite H; auto. Qed.
imports: MSetInterface OrdersFacts OrdersLists