proposition: Theorem isort_permutation : forall l : list A, Permutation l (isort l).
proof: Proof. intros l; elim l; clear l; simpl in |- *; auto. intros a l H'. apply Permutation_trans with (l' := a :: isort l); auto. Qed.
imports: Coq(List Sorting.Permutation) Huffman(Ordered)