proposition: Lemma partition_2 : forall s f, @compat_bool elt E.eq f -> Equal (snd (partition f s)) (filter (fun x => negb (f x)) s).
proof: Proof. intros. rewrite partition_filter. apply eq_refl. Qed.
imports: Bool PeanoNat BinPos OrderedType OrderedTypeEx FSetInterface