proposition: Theorem frequency_not_null : forall m (c : code), 1 < length (frequency_list A_eq_dec m) -> unique_prefix c -> in_alphabet m c -> not_null c.
proof: Proof. intros m c H H0 H1. case_eq (frequency_list A_eq_dec m); auto. intros H2; rewrite H2 in H; contradict H; simpl in |- *; auto with arith. intros p l; case p; case l; simpl in |- *; auto. intros a n H2; rewrite H2 in H; contradict H; simpl in |- *; auto with arith. intros p0 l0; case p0; intros b nb a na H2. apply unique_prefix_not_null with a b; auto. intros H3; absurd (In (fst (a, na)) (fst (b, nb) :: map (fst (B:=_)) l0)). cut (NoDup (map (fst (B:=_)) (frequency_list A_eq_dec m))). rewrite H2; simpl in |- *; intros H4; inversion H4. case H7; rewrite H3; auto with datatypes. apply unique_key_NoDup. apply frequency_list_unique. simpl in |- *; rewrite H3; auto with datatypes. case (H1 a); auto. apply frequency_list_in with A_eq_dec na; rewrite H2; auto with datatypes. intros l1 Hl1; apply in_alphabet_cons with l1; auto. case (H1 b); auto. apply frequency_list_in with A_eq_dec nb; rewrite H2; auto with datatypes. intros l2 Hl2; apply in_alphabet_cons with l2; auto. Qed.
imports: Coq(Sorting.Permutation)