proposition: Lemma in_quick_in : forall a l, In a l <-> In a (quicksort l).
proof: Proof. intros a l; apply in_permut_in. apply quick_permut. Qed.
imports: Coq(Relations Setoid List Multiset Arith Recdef Morphisms) CoLoR(more_list list_permut ordered_set)