proposition: Theorem quick_sorted : forall l, is_sorted (quicksort l).
proof: Proof. intros l; functional induction (quicksort l) as [ | l a' l' l_eq_a'_l' l1 l2 H S1 S2]. auto. apply quick_sorted_aux1; trivial. intros a a_in_ql1; assert (H1 := quick_sorted_aux3 l' a'); rewrite H in H1; apply H1. rewrite (mem_permut_mem a (quick_permut l1)); trivial. intros a a_in_ql2; assert (H2 := quick_sorted_aux4 l' a'); rewrite H in H2; apply H2; rewrite (mem_permut_mem a (quick_permut l2)); trivial. Qed.
imports: Coq(Relations Setoid List Multiset Arith Recdef Morphisms) CoLoR(more_list list_permut ordered_set)