proposition: Lemma partition_filter : forall s f, partition f s = (filter f s, filter (fun x => negb (f x)) s).
proof: Proof. unfold partition, filter. intros s f. generalize 1 as j. induction s as [|l IHl o r IHr]; intro j. - reflexivity. - destruct o; simpl; rewrite IHl, IHr; reflexivity. Qed.
imports: Bool PeanoNat BinPos Orders OrdersEx MSetInterface