fact: Fixpoint insert (a : A) (l : list A) {struct l} : list A := match l with | [] => a :: [] | b :: l1 => match order_fun a b with | true => a :: l | false => b :: insert a l1 end end.
imports: Coq(List Sorting.Permutation) Huffman(Ordered)