proposition: Lemma qs_sort (l : list A) : sort le (qs l).
proof: Proof. intros. funelim (qs l). constructor. apply sort_le_app; auto. constructor. auto. apply hdrel_filter. intros. simpl in H2. rewrite <- qs_same, filter_In' in H1, H2. intuition auto with arith. subst. pose (r:=refl_le x y); apply ltb_leb in H4; now depelim r. apply ltb_leb in H4. pose (r:=refl_le x a); pose (r':=refl_le a y); depelim r; depelim r'; reverse; DepElim.simplify_dep_elim; eauto. 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