proposition: Theorem quick_permut : forall l, permut l (quicksort l).
proof: Proof. intros l; functional induction (quicksort l) as [ | l a' l' l_eq_a'_l' l1 l2 H S1 S2]; auto. rewrite <- permut_cons_inside. assert (P := partition_list_permut1 a' l'); rewrite H in P. rewrite <- P; rewrite <- S1; rewrite <- S2; auto. reflexivity. Qed.
imports: Coq(Relations Setoid List Multiset Arith Recdef Morphisms) CoLoR(more_list list_permut ordered_set)