proposition: Theorem quick_permut_bis : forall l1 l2, permut l1 l2 -> permut (quicksort l1) l2.
proof: Proof. intros l1 l2 P; apply permut_trans with l1; trivial; apply permut_sym; apply quick_permut. Qed.
imports: Coq(Relations Setoid List Multiset Arith Recdef Morphisms) CoLoR(more_list list_permut ordered_set)