proposition: Theorem isort_ordered : forall l : list A, ordered order (isort l).
proof: Proof. Proof using order_fun_false order_fun_true. intros l; elim l; simpl in |- *; auto. Qed.
imports: Coq(List Sorting.Permutation) Huffman(Ordered)