proposition: Lemma Permutation_filter {A} (l : list A) (p : A -> bool) : Permutation l (filter p l ++ filter (compose negb p) l).
proof: Proof. Proof with simpl; intros. induction l; unfold compose; simpl; auto. case_eq (p a); simpl; intros; auto using Permutation_cons_app. Qed.
imports: Program Utf8 Equations.Prop.Equations Bvector List Relations Arith Wf_nat Lia Coq.Lists.SetoidList Coq.Sorting.Sorting Coq.Sorting.Permutation Coq.Sorting.PermutSetoid