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