proposition: Lemma partition_spec2 s f : Proper (X.eq==>Logic.eq) f -> Equal (snd (partition f s)) (filter (fun x => negb (f x)) s).
proof: Proof. now rewrite partition_spec. Qed.
imports: Bool List BinPos Pnat Setoid SetoidList PeanoNat