proposition: Lemma qs_perm l : Permutation l (qs l).
proof: Proof. funelim (qs l). constructor. intros. rewrite <- H0, <- H. apply Permutation_cons_app. rewrite Permutation_app_comm. apply Permutation_filter2. intros. case_eq (leb a x). simpl. intros. case_eq (ltb x a). intros. apply Is_true_eq_left in H2. apply Is_true_eq_left in H1. apply ltb_leb'' in H2. contradiction. constructor. simpl. intros. rewrite ltb_leb' in H1. case_eq (ltb x a). constructor. intros. rewrite H2 in H1. elim H1. 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 Bool EquivDec Permutation