proposition: Lemma qs_same (l : list A) : forall a, In a l <-> In a (qs l).
proof: Proof. funelim (qs l). - simpl. reflexivity. - intros a'. simpl. rewrite in_app_iff. simpl. rewrite <- H, <- H0, !filter_In'. intuition auto. destruct (compspec a a'); intuition auto. right. right. intuition auto with arith. apply ltb_leb. destruct (refl_lt a a'); auto. constructor. contradiction. left. intuition auto. destruct (refl_lt a' a); auto. constructor. contradiction. 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