proposition: Theorem number_of_occurrences_permutation_ex : forall (m : list A) (a : A), exists m1 : list A, Permutation m (id_list a (number_of_occurrences a m) ++ m1) /\ ~ In a m1.
proof: Proof. intros m; elim m; simpl in |- *; auto. intros a; exists []; split; auto with datatypes. intros a l H a0. case (A_eq_dec a0 a); simpl in |- *; intros H1. case (H a0); intros m1 (H2, H3). exists m1; split; auto. pattern a0 at 1 in |- *; rewrite H1; auto. case (H a0); intros m1 (H2, H3). exists (a :: m1); split; auto. apply Permutation_trans with ((a :: m1) ++ id_list a0 (number_of_occurrences a0 l)); auto. simpl in |- *; apply perm_skip; auto. apply Permutation_trans with (1 := H2); auto. simpl in |- *; contradict H3; case H3; intros H4; auto; case H1; auto. Qed.
imports: Coq(List Sorting.Permutation) Huffman(AuxLib UniqueKey)