proposition: Lemma filter_aux_elements s f acc : filter_aux f s acc = List.filter f (elements s) ++ acc.
proof: Proof. revert acc. induction s as [|c l IHl x r IHr]; trivial. intros acc. rewrite elements_node, List.filter_app. simpl. destruct (f x); now rewrite IHl, IHr, <- app_assoc. Qed.
imports: Bool List BinPos Pnat Setoid SetoidList PeanoNat