proposition: Lemma partition_aux_spec s f acc1 acc2 : partition_aux f s acc1 acc2 = (filter_aux f s acc1, filter_aux (fun x => negb (f x)) s acc2).
proof: Proof. revert acc1 acc2. induction s as [ | c l Hl x r Hr ]; simpl. - trivial. - intros acc1 acc2. destruct (f x); simpl; now rewrite Hr, Hl. Qed.
imports: Bool List BinPos Pnat Setoid SetoidList PeanoNat