proposition: Lemma length_quicksort : forall l, length (quicksort l) = length l.
proof: Proof. intro l; apply permut_length with EDS.eq_A; apply permut_sym; apply quick_permut. Qed.
imports: Coq(Relations Setoid List Multiset Arith Recdef Morphisms) CoLoR(more_list list_permut ordered_set)