proposition: Lemma partition_spec s f : partition f s = (filter f s, filter (fun x => negb (f x)) s).
proof: Proof. unfold partition, filter. now rewrite partition_aux_spec. Qed.
imports: Bool List BinPos Pnat Setoid SetoidList PeanoNat